src/HOL/ex/Arithmetic_Series_Complex.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 41959 b460124855b8
child 47222 1b7c909a6fad
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (*  Title:      HOL/ex/Arithmetic_Series_Complex.thy
     2     Author:     Benjamin Porter, 2006
     3 *)
     4 
     5 
     6 header {* Arithmetic Series for Reals *}
     7 
     8 theory Arithmetic_Series_Complex
     9 imports Complex_Main 
    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