equal
deleted
inserted
replaced
|
1 (* Title: HOL/Complex/ex/Arithmetic_Series_Complex |
|
2 ID: $Id$ |
|
3 Author: Benjamin Porter, 2006 |
|
4 *) |
|
5 |
|
6 |
|
7 header {* Arithmetic Series for Reals *} |
|
8 |
|
9 theory Arithmetic_Series_Complex |
|
10 imports Complex_Main Arithmetic_Series |
|
11 begin |
|
12 |
|
13 lemma arith_series_real: |
|
14 "(2::real) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = |
|
15 of_nat n * (a + (a + of_nat(n - 1)*d))" |
|
16 proof - |
|
17 have |
|
18 "((1::real) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat(i)*d) = |
|
19 of_nat(n) * (a + (a + of_nat(n - 1)*d))" |
|
20 by (rule arith_series_general) |
|
21 thus ?thesis by simp |
|
22 qed |
|
23 |
|
24 end |