author | wenzelm |
Sat, 09 Jul 2011 21:53:27 +0200 | |
changeset 43721 | fad8634cee62 |
parent 41959 | b460124855b8 |
child 47222 | 1b7c909a6fad |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/ex/Arithmetic_Series_Complex.thy |
19358 | 2 |
Author: Benjamin Porter, 2006 |
3 |
*) |
|
4 |
||
5 |
||
6 |
header {* Arithmetic Series for Reals *} |
|
7 |
||
8 |
theory Arithmetic_Series_Complex |
|
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19358
diff
changeset
|
9 |
imports Complex_Main |
19358 | 10 |
begin |
11 |
||
12 |
lemma arith_series_real: |
|
13 |
"(2::real) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = |
|
14 |
of_nat n * (a + (a + of_nat(n - 1)*d))" |
|
15 |
proof - |
|
16 |
have |
|
17 |
"((1::real) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat(i)*d) = |
|
18 |
of_nat(n) * (a + (a + of_nat(n - 1)*d))" |
|
19 |
by (rule arith_series_general) |
|
20 |
thus ?thesis by simp |
|
21 |
qed |
|
22 |
||
23 |
end |