src/HOL/Complex/ex/ASeries_Complex.thy

* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
* added Complex/ex/ASeries_Complex (instantiation of the above for reals)
* added Complex/ex/HarmonicSeries (should really be in something like Complex/Library)

(these are contributions by Benjamin Porter, numbers 68 and 34 of
http://www.cs.ru.nl/~freek/100/)

(*  Title:      HOL/Library/ASeries.thy
    ID:         $Id$
    Author:     Benjamin Porter, 2006
*)


header {* Arithmetic Series for Reals *}

theory ASeries_Complex
imports Complex_Main ASeries
begin

lemma arith_series_real:
  "(2::real) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
  of_nat n * (a + (a + of_nat(n - 1)*d))"
proof -
  have
    "((1::real) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat(i)*d) =
    of_nat(n) * (a + (a + of_nat(n - 1)*d))"
    by (rule arith_series_general)
  thus ?thesis by simp
qed

end