author | haftmann |
Wed, 10 Feb 2010 08:49:26 +0100 | |
changeset 35084 | e25eedfc15ce |
parent 28952 | 15a4b2cf8c34 |
child 41959 | b460124855b8 |
permissions | -rw-r--r-- |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
19469
diff
changeset
|
1 |
(* Title: HOL/ex/Arithmetic_Series_Complex |
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 |