src/HOL/ex/Arithmetic_Series_Complex.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 28952 15a4b2cf8c34
child 41959 b460124855b8
permissions -rw-r--r--
added lemmas
haftmann@28952
     1
(*  Title:      HOL/ex/Arithmetic_Series_Complex
kleing@19358
     2
    Author:     Benjamin Porter, 2006
kleing@19358
     3
*)
kleing@19358
     4
kleing@19358
     5
kleing@19358
     6
header {* Arithmetic Series for Reals *}
kleing@19358
     7
kleing@19358
     8
theory Arithmetic_Series_Complex
kleing@19469
     9
imports Complex_Main 
kleing@19358
    10
begin
kleing@19358
    11
kleing@19358
    12
lemma arith_series_real:
kleing@19358
    13
  "(2::real) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
kleing@19358
    14
  of_nat n * (a + (a + of_nat(n - 1)*d))"
kleing@19358
    15
proof -
kleing@19358
    16
  have
kleing@19358
    17
    "((1::real) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat(i)*d) =
kleing@19358
    18
    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
kleing@19358
    19
    by (rule arith_series_general)
kleing@19358
    20
  thus ?thesis by simp
kleing@19358
    21
qed
kleing@19358
    22
kleing@19358
    23
end