isabelle: src/HOL/ex/Arithmetic_Series_Complex.thy@9c68004b8c9d (annotated)

28952 15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 19469 diff changeset	1	(* Title: HOL/ex/Arithmetic_Series_Complex
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	blanchet
	Wed, 15 Dec 2010 11:26:28 +0100
changeset 41140	9c68004b8c9d
parent 28952	15a4b2cf8c34
child 41959	b460124855b8
permissions	-rw-r--r--