isabelle: src/HOL/ex/Arithmetic_Series_Complex.thy@5bdd68f380b3 (annotated)

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

author	wenzelm
	Thu, 08 Mar 2012 19:56:57 +0100
changeset 46837	5bdd68f380b3
parent 41959	b460124855b8
child 47222	1b7c909a6fad
permissions	-rw-r--r--