Theorem geolimilem 7358

Description: Lemma for geolimi 7359.

Hypotheses

Ref	Expression
geoser.1	|- F = {<.k, y>. | (k e. NN0 /\ y = (A^k))}
geoser.2	|- A e. CC
geolimilem.3	|- (abs` A) < 1
geolimilem.4	|- G Fn NN0
geolimilem.5	|- (n e. NN0 -> (G` n) = (-u(A x. (F` n)) / (1 - A)))

Assertion

Ref	Expression
geolimilem	|- ( + seq0 F) ~~> (1 / (1 - A))

Distinct variable groups:   k,n,y,A   n,F   n,G

Proof of Theorem geolimilem

Step	Hyp	Ref	Expression
1		ax1cn 5358	. . . . . . . . . . 11 |- 1 e. CC
2		geoser.2	. . . . . . . . . . 11 |- A e. CC
3	1, 2	subcli 5455	. . . . . . . . . 10 |- (1 - A) e. CC
4		1re 5524	. . . . . . . . . . 11 |- 1 e. RR
5		geolimilem.3	. . . . . . . . . . 11 |- (abs` A) < 1
6		abssubne0 7005	. . . . . . . . . . 11 |- ((A e. CC /\ 1 e. RR /\ (abs` A) < 1) -> (1 - A) =/= 0)
7	2, 4, 5, 6	mp3an 919	. . . . . . . . . 10 |- (1 - A) =/= 0
8	3, 7	reccli 5802	. . . . . . . . 9 |- (1 / (1 - A)) e. CC
9	8	negcli 5458	. . . . . . . 8 |- -u(1 / (1 - A)) e. CC
10	9, 2	mulcli 5410	. . . . . . 7 |- (-u(1 / (1 - A)) x. A) e. CC
11		nnnn0 6216	. . . . . . . . . 10 |- (n e. NN -> n e. NN0)
12		opreq2 4045	. . . . . . . . . . 11 |- (k = n -> (A^k) = (A^n))
13		geoser.1	. . . . . . . . . . 11 |- F = {<.k, y>. | (k e. NN0 /\ y = (A^k))}
14		oprex 4059	. . . . . . . . . . 11 |- (A^n) e. V
15	12, 13, 14	fvopab4 3856	. . . . . . . . . 10 |- (n e. NN0 -> (F` n) = (A^n))
16	11, 15	syl 10	. . . . . . . . 9 |- (n e. NN -> (F` n) = (A^n))
17	16	rgen 1736	. . . . . . . 8 |- A.n e. NN (F` n) = (A^n)
18		nn0ex 6215	. . . . . . . . . 10 |- NN0 e. V
19	18, 13	fopabex2 3687	. . . . . . . . 9 |- F e. V
20	19	expcnv 7356	. . . . . . . 8 |- ((A e. CC /\ A.n e. NN (F` n) = (A^n) /\ (abs` A) < 1) -> F ~~> 0)
21	2, 17, 5, 20	mp3an 919	. . . . . . 7 |- F ~~> 0
22	10, 21	pm3.2i 283	. . . . . 6 |- ((-u(1 / (1 - A)) x. A) e. CC /\ F ~~> 0)
23		0z 6256	. . . . . . 7 |- 0 e. ZZ
24		elnn0uz 6501	. . . . . . . . 9 |- (n e. NN0 <-> n e. (ZZ>` 0))
25		expcl 6704	. . . . . . . . . . . . 13 |- ((A e. CC /\ k e. NN0) -> (A^k) e. CC)
26	2, 25	mpan 698	. . . . . . . . . . . 12 |- (k e. NN0 -> (A^k) e. CC)
27	13, 26	fopab 3903	. . . . . . . . . . 11 |- F:NN0-->CC
28	27	ffvelrni 3891	. . . . . . . . . 10 |- (n e. NN0 -> (F` n) e. CC)
29		geolimilem.5	. . . . . . . . . . 11 |- (n e. NN0 -> (G` n) = (-u(A x. (F` n)) / (1 - A)))
30	2	negcli 5458	. . . . . . . . . . . . . 14 |- -uA e. CC
31	3, 7	pm3.2i 283	. . . . . . . . . . . . . 14 |- ((1 - A) e. CC /\ (1 - A) =/= 0)
32		div23 5826	. . . . . . . . . . . . . 14 |- ((-uA e. CC /\ (F` n) e. CC /\ ((1 - A) e. CC /\ (1 - A) =/= 0)) -> ((-uA x. (F` n)) / (1 - A)) = ((-uA / (1 - A)) x. (F` n)))
33	30, 31, 32	mp3an13 910	. . . . . . . . . . . . 13 |- ((F` n) e. CC -> ((-uA x. (F` n)) / (1 - A)) = ((-uA / (1 - A)) x. (F` n)))
34	28, 33	syl 10	. . . . . . . . . . . 12 |- (n e. NN0 -> ((-uA x. (F` n)) / (1 - A)) = ((-uA / (1 - A)) x. (F` n)))
35		mulneg1 5540	. . . . . . . . . . . . . . 15 |- ((A e. CC /\ (F` n) e. CC) -> (-uA x. (F` n)) = -u(A x. (F` n)))
36	2, 35	mpan 698	. . . . . . . . . . . . . 14 |- ((F` n) e. CC -> (-uA x. (F` n)) = -u(A x. (F` n)))
37	28, 36	syl 10	. . . . . . . . . . . . 13 |- (n e. NN0 -> (-uA x. (F` n)) = -u(A x. (F` n)))
38	37	opreq1d 4051	. . . . . . . . . . . 12 |- (n e. NN0 -> ((-uA x. (F` n)) / (1 - A)) = (-u(A x. (F` n)) / (1 - A)))
39		mulneg12 5542	. . . . . . . . . . . . . . . . 17 |- (((1 / (1 - A)) e. CC /\ A e. CC) -> (-u(1 / (1 - A)) x. A) = ((1 / (1 - A)) x. -uA))
40	8, 2, 39	mp2an 700	. . . . . . . . . . . . . . . 16 |- (-u(1 / (1 - A)) x. A) = ((1 / (1 - A)) x. -uA)
41		divrec2 5823	. . . . . . . . . . . . . . . . 17 |- ((-uA e. CC /\ (1 - A) e. CC /\ (1 - A) =/= 0) -> (-uA / (1 - A)) = ((1 / (1 - A)) x. -uA))
42	30, 3, 7, 41	mp3an 919	. . . . . . . . . . . . . . . 16 |- (-uA / (1 - A)) = ((1 / (1 - A)) x. -uA)
43	40, 42	eqtr4i 1535	. . . . . . . . . . . . . . 15 |- (-u(1 / (1 - A)) x. A) = (-uA / (1 - A))
44	43	opreq1i 4047	. . . . . . . . . . . . . 14 |- ((-u(1 / (1 - A)) x. A) x. (F` n)) = ((-uA / (1 - A)) x. (F` n))
45	44	eqcomi 1516	. . . . . . . . . . . . 13 |- ((-uA / (1 - A)) x. (F` n)) = ((-u(1 / (1 - A)) x. A) x. (F` n))
46	45	a1i 8	. . . . . . . . . . . 12 |- (n e. NN0 -> ((-uA / (1 - A)) x. (F` n)) = ((-u(1 / (1 - A)) x. A) x. (F` n)))
47	34, 38, 46	3eqtr3d 1552	. . . . . . . . . . 11 |- (n e. NN0 -> (-u(A x. (F` n)) / (1 - A)) = ((-u(1 / (1 - A)) x. A) x. (F` n)))
48	29, 47	eqtrd 1544	. . . . . . . . . 10 |- (n e. NN0 -> (G` n) = ((-u(1 / (1 - A)) x. A) x. (F` n)))
49	28, 48	jca 286	. . . . . . . . 9 |- (n e. NN0 -> ((F` n) e. CC /\ (G` n) = ((-u(1 / (1 - A)) x. A) x. (F` n))))
50	24, 49	sylbir 199	. . . . . . . 8 |- (n e. (ZZ>` 0) -> ((F` n) e. CC /\ (G` n) = ((-u(1 / (1 - A)) x. A) x. (F` n))))
51	50	rgen 1736	. . . . . . 7 |- A.n e. (ZZ>` 0)((F` n) e. CC /\ (G` n) = ((-u(1 / (1 - A)) x. A) x. (F` n)))
52	23, 51	pm3.2i 283	. . . . . 6 |- (0 e. ZZ /\ A.n e. (ZZ>` 0)((F` n) e. CC /\ (G` n) = ((-u(1 / (1 - A)) x. A) x. (F` n))))
53		geolimilem.4	. . . . . . . 8 |- G Fn NN0
54		fnex 3682	. . . . . . . 8 |- ((G Fn NN0 /\ NN0 e. V) -> G e. V)
55	53, 18, 54	mp2an 700	. . . . . . 7 |- G e. V
56	23	elisseti 1856	. . . . . . 7 |- 0 e. V
57	19, 55, 56	climmulc2 7252	. . . . . 6 |- ((((-u(1 / (1 - A)) x. A) e. CC /\ F ~~> 0) /\ (0 e. ZZ /\ A.n e. (ZZ>` 0)((F` n) e. CC /\ (G` n) = ((-u(1 / (1 - A)) x. A) x. (F` n))))) -> G ~~> ((-u(1 / (1 - A)) x. A) x. 0))
58	22, 52, 57	mp2an 700	. . . . 5 |- G ~~> ((-u(1 / (1 - A)) x. A) x. 0)
59	10	mul01i 5520	. . . . 5 |- ((-u(1 / (1 - A)) x. A) x. 0) = 0
60	58, 59	breqtri 2688	. . . 4 |- G ~~> 0
61	60, 8	pm3.2i 283	. . 3 |- (G ~~> 0 /\ (1 / (1 - A)) e. CC)
62		mulcl 5392	. . . . . . . . . . . 12 |- ((A e. CC /\ (F` n) e. CC) -> (A x. (F` n)) e. CC)
63	2, 62	mpan 698	. . . . . . . . . . 11 |- ((F` n) e. CC -> (A x. (F` n)) e. CC)
64	28, 63	syl 10	. . . . . . . . . 10 |- (n e. NN0 -> (A x. (F` n)) e. CC)
65		negcl 5457	. . . . . . . . . 10 |- ((A x. (F` n)) e. CC -> -u(A x. (F` n)) e. CC)
66	64, 65	syl 10	. . . . . . . . 9 |- (n e. NN0 -> -u(A x. (F` n)) e. CC)
67		divcl 5801	. . . . . . . . . 10 |- ((-u(A x. (F` n)) e. CC /\ (1 - A) e. CC /\ (1 - A) =/= 0) -> (-u(A x. (F` n)) / (1 - A)) e. CC)
68	3, 7, 67	mp3an23 911	. . . . . . . . 9 |- (-u(A x. (F` n)) e. CC -> (-u(A x. (F` n)) / (1 - A)) e. CC)
69	66, 68	syl 10	. . . . . . . 8 |- (n e. NN0 -> (-u(A x. (F` n)) / (1 - A)) e. CC)
70	29, 69	eqeltrd 1585	. . . . . . 7 |- (n e. NN0 -> (G` n) e. CC)
71		expcl 6704	. . . . . . . . . . . . . . 15 |- ((A e. CC /\ n e. NN0) -> (A^n) e. CC)
72	2, 71	mpan 698	. . . . . . . . . . . . . 14 |- (n e. NN0 -> (A^n) e. CC)
73		mulcom 5395	. . . . . . . . . . . . . . 15 |- ((A e. CC /\ (A^n) e. CC) -> (A x. (A^n)) = ((A^n) x. A))
74	2, 73	mpan 698	. . . . . . . . . . . . . 14 |- ((A^n) e. CC -> (A x. (A^n)) = ((A^n) x. A)