src/HOL/ex/Arithmetic_Series_Complex.thy
author huffman
Fri Aug 19 14:17:28 2011 -0700 (2011-08-19)
changeset 44311 42c5cbf68052
parent 41959 b460124855b8
child 47222 1b7c909a6fad
permissions -rw-r--r--
Transcendental.thy: add tendsto_intros lemmas;
new isCont theorems;
simplify some proofs.
wenzelm@41959
     1
(*  Title:      HOL/ex/Arithmetic_Series_Complex.thy
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