isabelle: src/HOL/Complex/ex/Arithmetic_Series_Complex.thy@1b0f4e6f81aa (annotated)

19358 9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	1	(* Title: HOL/Complex/ex/Arithmetic_Series_Complex
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	2	ID: $Id$
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	3	Author: Benjamin Porter, 2006
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	4	*)
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	5
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	6
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	7	header {* Arithmetic Series for Reals *}
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	8
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	9	theory Arithmetic_Series_Complex
19469 958d2f2dd8d4 moved arithmetic series to geometric series in SetInterval kleing parents: 19358 diff changeset	10	imports Complex_Main
19358 9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	11	begin
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	12
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	13	lemma arith_series_real:
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	14	"(2::real) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) =
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	15	of_nat n * (a + (a + of_nat(n - 1)*d))"
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	16	proof -
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	17	have
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	18	"((1::real) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat(i)*d) =
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	19	of_nat(n) * (a + (a + of_nat(n - 1)*d))"
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	20	by (rule arith_series_general)
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	21	thus ?thesis by simp
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	22	qed
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	23
9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: diff changeset	24	end

author	wenzelm
	Wed, 09 May 2007 19:37:18 +0200
changeset 22893	1b0f4e6f81aa
parent 19469	958d2f2dd8d4
permissions	-rw-r--r--