Theorem geolimilem 7187

Description: Lemma for geolimi 7188.

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 5252	. . . . . . . . . . 11 |- 1 e. CC
2		geoser.2	. . . . . . . . . . 11 |- A e. CC
3	1, 2	subcl 5349	. . . . . . . . . 10 |- (1 - A) e. CC
4		1re 5418	. . . . . . . . . . 11 |- 1 e. RR
5		geolimilem.3	. . . . . . . . . . 11 |- (abs` A) < 1
6		abssubne0t 6835	. . . . . . . . . . 11 |- ((A e. CC /\ 1 e. RR /\ (abs` A) < 1) -> (1 - A) =/= 0)
7	2, 4, 5, 6	mp3an 915	. . . . . . . . . 10 |- (1 - A) =/= 0
8	3, 7	reccl 5692	. . . . . . . . 9 |- (1 / (1 - A)) e. CC
9	8	negcl 5352	. . . . . . . 8 |- -u(1 / (1 - A)) e. CC
10	9, 2	mulcl 5304	. . . . . . 7 |- (-u(1 / (1 - A)) x. A) e. CC
11		nnnn0t 6063	. . . . . . . . . 10 |- (n e. NN -> n e. NN0)
12		opreq2 3964	. . . . . . . . . . 11 |- (k = n -> (A^k) = (A^n))
13		geoser.1	. . . . . . . . . . 11 |- F = {<.k, y>. | (k e. NN0 /\ y = (A^k))}
14		oprex 3978	. . . . . . . . . . 11 |- (A^n) e. V
15	12, 13, 14	fvopab4 3775	. . . . . . . . . 10 |- (n e. NN0 -> (F` n) = (A^n))
16	11, 15	syl 10	. . . . . . . . 9 |- (n e. NN -> (F` n) = (A^n))
17	16	rgen 1696	. . . . . . . 8 |- A.n e. NN (F` n) = (A^n)
18		nn0ex 6062	. . . . . . . . . 10 |- NN0 e. V
19	18, 13	fopabex2 3608	. . . . . . . . 9 |- F e. V
20	19	expcnv 7185	. . . . . . . 8 |- ((A e. CC /\ A.n e. NN (F` n) = (A^n) /\ (abs` A) < 1) -> F ~~> 0)
21	2, 17, 5, 20	mp3an 915	. . . . . . 7 |- F ~~> 0
22	10, 21	pm3.2i 285	. . . . . 6 |- ((-u(1 / (1 - A)) x. A) e. CC /\ F ~~> 0)
23		0z 6103	. . . . . . 7 |- 0 e. ZZ
24		elnn0uz 6386	. . . . . . . . 9 |- (n e. NN0 <-> n e. (ZZ>` 0))
25		expclt 6526	. . . . . . . . . . . . 13 |- ((A e. CC /\ k e. NN0) -> (A^k) e. CC)
26	2, 25	mpan 694	. . . . . . . . . . . 12 |- (k e. NN0 -> (A^k) e. CC)
27	13, 26	fopab 3822	. . . . . . . . . . 11 |- F:NN0-->CC
28	27	ffvelrni 3810	. . . . . . . . . 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	negcl 5352	. . . . . . . . . . . . . 14 |- -uA e. CC
31		div23t 5715	. . . . . . . . . . . . . . 15 |- (((-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)))
32	7, 31	mpan2 695	. . . . . . . . . . . . . 14 |- ((-uA e. CC /\ (F` n) e. CC /\ (1 - A) e. CC) -> ((-uA x. (F` n)) / (1 - A)) = ((-uA / (1 - A)) x. (F` n)))
33	30, 3, 32	mp3an13 906	. . . . . . . . . . . . 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		mulneg1t 5434	. . . . . . . . . . . . . . 15 |- ((A e. CC /\ (F` n) e. CC) -> (-uA x. (F` n)) = -u(A x. (F` n)))
36	2, 35	mpan 694	. . . . . . . . . . . . . 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 3970	. . . . . . . . . . . 12 |- (n e. NN0 -> ((-uA x. (F` n)) / (1 - A)) = (-u(A x. (F` n)) / (1 - A)))
39		mulneg12t 5436	. . . . . . . . . . . . . . . . 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 696	. . . . . . . . . . . . . . . 16 |- (-u(1 / (1 - A)) x. A) = ((1 / (1 - A)) x. -uA)
41		divrec2t 5713	. . . . . . . . . . . . . . . . 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 915	. . . . . . . . . . . . . . . 16 |- (-uA / (1 - A)) = ((1 / (1 - A)) x. -uA)
43	40, 42	eqtr4 1496	. . . . . . . . . . . . . . 15 |- (-u(1 / (1 - A)) x. A) = (-uA / (1 - A))
44	43	opreq1i 3966	. . . . . . . . . . . . . 14 |- ((-u(1 / (1 - A)) x. A) x. (F` n)) = ((-uA / (1 - A)) x. (F` n))
45	44	eqcomi 1477	. . . . . . . . . . . . 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 1513	. . . . . . . . . . 11 |- (n e. NN0 -> (-u(A x. (F` n)) / (1 - A)) = ((-u(1 / (1 - A)) x. A) x. (F` n)))
48	29, 47	eqtrd 1505	. . . . . . . . . 10 |- (n e. NN0 -> (G` n) = ((-u(1 / (1 - A)) x. A) x. (F` n)))
49	28, 48	jca 288	. . . . . . . . 9 |- (n e. NN0 -> ((F` n) e. CC /\ (G` n) = ((-u(1 / (1 - A)) x. A) x. (F` n))))
50	24, 49	sylbir 201	. . . . . . . 8 |- (n e. (ZZ>` 0) -> ((F` n) e. CC /\ (G` n) = ((-u(1 / (1 - A)) x. A) x. (F` n))))
51	50	rgen 1696	. . . . . . 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 285	. . . . . 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 3603	. . . . . . . 8 |- ((G Fn NN0 /\ NN0 e. V) -> G e. V)
55	53, 18, 54	mp2an 696	. . . . . . 7 |- G e. V
56	23	elisseti 1815	. . . . . . 7 |- 0 e. V
57	19, 55, 56	climmulc2 7082	. . . . . 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 696	. . . . 5 |- G ~~> ((-u(1 / (1 - A)) x. A) x. 0)
59	10	mul01 5414	. . . . 5 |- ((-u(1 / (1 - A)) x. A) x. 0) = 0
60	58, 59	breqtr 2634	. . . 4 |- G ~~> 0
61	60, 8	pm3.2i 285	. . 3 |- (G ~~> 0 /\ (1 / (1 - A)) e. CC)
62		axmulcl 5256	. . . . . . . . . . . 12 |- ((A e. CC /\ (F` n) e. CC) -> (A x. (F` n)) e. CC)
63	2, 62	mpan 694	. . . . . . . . . . 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		negclt 5351	. . . . . . . . . 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		divclt 5691	. . . . . . . . . 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 907	. . . . . . . . 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 1546	. . . . . . 7 |- (n e. NN0 -> (G` n) e. CC)
71		expclt 6526	. . . . . . . . . . . . . . 15 |- ((A e. CC /\ n e. NN0) -> (A^n) e. CC)
72	2, 71	mpan 694	. . . . . . . . . . . . . 14 |- (n e. NN0 -> (A^n) e. CC)
73		axmulcom 5259	. . . . . . . . . . . . . . 15 |- ((A e. CC /\ (A^n) e. CC) -> (A x. (A^n)