Theorem geolim1i 7223

Description: The partial sums in the geometric series A^1 + A^2... converge to (A / (1 - A)).

Hypotheses

Ref	Expression
geolim1i.1	|- F = {<.k, y>. | (k e. NN /\ y = (A^k))}
geolim1i.2	|- A e. CC
geolim1i.3	|- (abs` A) < 1

Assertion

Ref	Expression
geolim1i	|- ( + seq1 F) ~~> (A / (1 - A))

Distinct variable group:   y,k,A

Proof of Theorem geolim1i

Step	Hyp	Ref	Expression
1		0z 6134	. . . 4 |- 0 e. ZZ
2		uzidt 6413	. . . 4 |- (0 e. ZZ -> 0 e. (ZZ>` 0))
3	1, 2	ax-mp 7	. . 3 |- 0 e. (ZZ>` 0)
4		nn0ex 6093	. . . . 5 |- NN0 e. V
5	4	opabex2 3610	. . . 4 |- {<.k, y>. | (k e. NN0 /\ y = (A^k))} e. V
6		oprex 3983	. . . 4 |- (1 / (1 - A)) e. V
7		addex 5309	. . . . . 6 |- + e. V
8	7, 5	seq0seqz 6528	. . . . 5 |- ( + seq0 {<.k, y>. | (k e. NN0 /\ y = (A^k))}) = (<.0, + >. seq {<.k, y>. | (k e. NN0 /\ y = (A^k))})
9		eqid 1475	. . . . . 6 |- {<.k, y>. | (k e. NN0 /\ y = (A^k))} = {<.k, y>. | (k e. NN0 /\ y = (A^k))}
10		geolim1i.2	. . . . . 6 |- A e. CC
11		geolim1i.3	. . . . . 6 |- (abs` A) < 1
12	9, 10, 11	geolimi 7221	. . . . 5 |- ( + seq0 {<.k, y>. | (k e. NN0 /\ y = (A^k))}) ~~> (1 / (1 - A))
13	8, 12	eqbrtrr 2636	. . . 4 |- (<.0, + >. seq {<.k, y>. | (k e. NN0 /\ y = (A^k))}) ~~> (1 / (1 - A))
14		expclt 6567	. . . . . . 7 |- ((A e. CC /\ k e. NN0) -> (A^k) e. CC)
15	10, 14	mpan 695	. . . . . 6 |- (k e. NN0 -> (A^k) e. CC)
16	9, 15	fopab 3827	. . . . 5 |- {<.k, y>. | (k e. NN0 /\ y = (A^k))}:NN0-->CC
17		nn0uz 6424	. . . . . 6 |- NN0 = (ZZ>` 0)
18		feq2 3621	. . . . . 6 |- (NN0 = (ZZ>` 0) -> ({<.k, y>. | (k e. NN0 /\ y = (A^k))}:NN0-->CC <-> {<.k, y>. | (k e. NN0 /\ y = (A^k))}:(ZZ>` 0)-->CC))
19	17, 18	ax-mp 7	. . . . 5 |- ({<.k, y>. | (k e. NN0 /\ y = (A^k))}:NN0-->CC <-> {<.k, y>. | (k e. NN0 /\ y = (A^k))}:(ZZ>` 0)-->CC)
20	16, 19	mpbi 189	. . . 4 |- {<.k, y>. | (k e. NN0 /\ y = (A^k))}:(ZZ>` 0)-->CC
21	5, 6, 13, 20	clim2serz 7130	. . 3 |- (0 e. (ZZ>` 0) -> (<.(0 + 1), + >. seq {<.k, y>. | (k e. NN0 /\ y = (A^k))}) ~~> ((1 / (1 - A)) - ((<.0, + >. seq {<.k, y>. | (k e. NN0 /\ y = (A^k))})` 0)))
22	3, 21	ax-mp 7	. 2 |- (<.(0 + 1), + >. seq {<.k, y>. | (k e. NN0 /\ y = (A^k))}) ~~> ((1 / (1 - A)) - ((<.0, + >. seq {<.k, y>. | (k e. NN0 /\ y = (A^k))})` 0))
23		geolim1i.1	. . . . . 6 |- F = {<.k, y>. | (k e. NN /\ y = (A^k))}
24		nnssnn0 6090	. . . . . . 7 |- NN (_ NN0
25		resopab2 3398	. . . . . . 7 |- (NN (_ NN0 -> ({<.k, y>. | (k e. NN0 /\ y = (A^k))} |` NN) = {<.k, y>. | (k e. NN /\ y = (A^k))})
26	24, 25	ax-mp 7	. . . . . 6 |- ({<.k, y>. | (k e. NN0 /\ y = (A^k))} |` NN) = {<.k, y>. | (k e. NN /\ y = (A^k))}
27		nnuz 6425	. . . . . . 7 |- NN = (ZZ>` 1)
28		reseq2 3369	. . . . . . 7 |- (NN = (ZZ>` 1) -> ({<.k, y>. | (k e. NN0 /\ y = (A^k))} |` NN) = ({<.k, y>. | (k e. NN0 /\ y = (A^k))} |` (ZZ>` 1)))
29	27, 28	ax-mp 7	. . . . . 6 |- ({<.k, y>. | (k e. NN0 /\ y = (A^k))} |` NN) = ({<.k, y>. | (k e. NN0 /\ y = (A^k))} |` (ZZ>` 1))
30	23, 26, 29	3eqtr2 1501	. . . . 5 |- F = ({<.k, y>. | (k e. NN0 /\ y = (A^k))} |` (ZZ>` 1))
31	30	opreq2i 3972	. . . 4 |- (<.1, + >. seq F) = (<.1, + >. seq ({<.k, y>. | (k e. NN0 /\ y = (A^k))} |` (ZZ>` 1)))
32		1z 6147	. . . . 5 |- 1 e. ZZ
33	7, 5	seqzres 6546	. . . . 5 |- (1 e. ZZ -> (<.1, + >. seq ({<.k, y>. | (k e. NN0 /\ y = (A^k))} |` (ZZ>` 1))) = (<.1, + >. seq {<.k, y>. | (k e. NN0 /\ y = (A^k))}))
34	32, 33	ax-mp 7	. . . 4 |- (<.1, + >. seq ({<.k, y>. | (k e. NN0 /\ y = (A^k))} |` (ZZ>` 1))) = (<.1, + >. seq {<.k, y>. | (k e. NN0 /\ y = (A^k))})
35	31, 34	eqtr 1495	. . 3 |- (<.1, + >. seq F) = (<.1, + >. seq {<.k, y>. | (k e. NN0 /\ y = (A^k))})
36		nnex 5921	. . . . 5 |- NN e. V
37	36, 23	fopabex2 3612	. . . 4 |- F e. V
38	7, 37	seq1seqz 6527	. . 3 |- ( + seq1 F) = (<.1, + >. seq F)
39		ax1cn 5261	. . . . . 6 |- 1 e. CC
40	39	addid2 5323	. . . . 5 |- (0 + 1) = 1
41	40	opeq1i 2490	. . . 4 |- <.(0 + 1), + >. = <.1, + >.
42	41	opreq1i 3971	. . 3 |- (<.(0 + 1), + >. seq {<.k, y>. | (k e. NN0 /\ y = (A^k))}) = (<.1, + >. seq {<.k, y>. | (k e. NN0 /\ y = (A^k))})
43	35, 38, 42	3eqtr4 1505	. 2 |- ( + seq1 F) = (<.(0 + 1), + >. seq {<.k, y>. | (k e. NN0 /\ y = (A^k))})
44	39, 10	subcl 5358	. . . . . 6 |- (1 - A) e. CC
45	39, 44, 44	3pm3.2i 818	. . . . 5 |- (1 e. CC /\ (1 - A) e. CC /\ (1 - A) e. CC)
46		1re 5427	. . . . . 6 |- 1 e. RR
47		abssubne0t 6867	. . . . . 6 |- ((A e. CC /\ 1 e. RR /\ (abs` A) < 1) -> (1 - A) =/= 0)
48	10, 46, 11, 47	mp3an 916	. . . . 5 |- (1 - A) =/= 0
49		divsubdirtOLD 5763	. . . . 5 |- (((1 e. CC /\ (1 - A) e. CC /\ (1 - A) e. CC) /\ (1 - A) =/= 0) -> ((1 - (1 - A)) / (1 - A)) = ((1 / (1 - A)) - ((1 - A) / (1 - A))))
50	45, 48, 49	mp2an 697	. . . 4 |- ((1 - (1 - A)) / (1 - A)) = ((1 / (1 - A)) - ((1 - A) / (1 - A)))
51		nncant 5461	. . . . . 6 |- ((1 e. CC /\ A e. CC) -> (1 - (1 - A)) = A)
52	39, 10, 51	mp2an 697	. . . . 5 |- (1 - (1 - A)) = A
53	52	opreq1i 3971	. . . 4 |- ((1 - (1 - A)) / (1 - A)) = (A / (1 - A))
54	44, 48	divid 5758	. . . . 5 |- ((1 - A) / (1 - A)) = 1
55	54	opreq2i 3972	. . . 4 |- ((1 / (1 - A)) - ((1 - A) / (1 - A))) = ((1 / (1 - A)) - 1)
56	50, 53, 55	3eqtr3 1503	. . 3 |- (A / (1 - A)) = ((1 / (1 - A)) - 1)
57	7, 5	seqz1 6533	. . . . . 6 |- (0 e. ZZ -> ((<.0, + >. seq {<.k, y>. | (k e. NN0 /\ y = (A^k))})` 0) = ({<.k, y>. | (k e. NN0 /\ y = (A^k))}` 0))
58	1, 57	ax-mp 7	. . . . 5 |- ((<.0, + >. seq {<.k, y>. | (k e. NN0 /\ y = (A^k))})` 0) = ({<.k, y>. | (k e. NN0 /\ y = (A^k))}` 0)
59		0nn0 6101	. . . . . 6 |- 0 e. NN0
60		opreq2 3969	. . . . . . 7 |- (k = 0 -> (A^k) = (A^0))
61		oprex 3983	. . . . . . 7 |- (A^0) e. V
62	60, 9, 61	fvopab4 3780	. . . . . 6 |- (0 e. NN0 -> ({<.k, y>. | (k e. NN0 /\ y = (A^k))}` 0) = (A^0))
63	59, 62	ax-mp 7	. . . . 5 |- ({<.k, y>. | (k e. NN0 /\ y = (A^k))}` 0) = (A^0)
64		exp0t 6557	. . . . . 6 |- (A e. CC -> (A^0) = 1)
65	10, 64	ax-mp 7	. . . . 5 |- (A^0) = 1