HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

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
StepHypRef Expression
1 ax1cn 5358 . . . . . . . . . . 11 |- 1 e. CC
2 geoser.2 . . . . . . . . . . 11 |- A e. CC
31, 2subcli 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)
72, 4, 5, 6mp3an 919 . . . . . . . . . 10 |- (1 - A) =/= 0
83, 7reccli 5802 . . . . . . . . 9 |- (1 / (1 - A)) e. CC
98negcli 5458 . . . . . . . 8 |- -u(1 / (1 - A)) e. CC
109, 2mulcli 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
1512, 13, 14fvopab4 3856 . . . . . . . . . 10 |- (n e. NN0 -> (F` n) = (A^n))
1611, 15syl 10 . . . . . . . . 9 |- (n e. NN -> (F` n) = (A^n))
1716rgen 1736 . . . . . . . 8 |- A.n e. NN (F` n) = (A^n)
18 nn0ex 6215 . . . . . . . . . 10 |- NN0 e. V
1918, 13fopabex2 3687 . . . . . . . . 9 |- F e. V
2019expcnv 7356 . . . . . . . 8 |- ((A e. CC /\ A.n e. NN (F` n) = (A^n) /\ (abs` A) < 1) -> F ~~> 0)
212, 17, 5, 20mp3an 919 . . . . . . 7 |- F ~~> 0
2210, 21pm3.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)
262, 25mpan 698 . . . . . . . . . . . 12 |- (k e. NN0 -> (A^k) e. CC)
2713, 26fopab 3903 . . . . . . . . . . 11 |- F:NN0-->CC
2827ffvelrni 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)))
302negcli 5458 . . . . . . . . . . . . . 14 |- -uA e. CC
313, 7pm3.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)))
3330, 31, 32mp3an13 910 . . . . . . . . . . . . 13 |- ((F` n) e. CC -> ((-uA x. (F` n)) / (1 - A)) = ((-uA / (1 - A)) x. (F` n)))
3428, 33syl 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)))
362, 35mpan 698 . . . . . . . . . . . . . 14 |- ((F` n) e. CC -> (-uA x. (F` n)) = -u(A x. (F` n)))
3728, 36syl 10 . . . . . . . . . . . . 13 |- (n e. NN0 -> (-uA x. (F` n)) = -u(A x. (F` n)))
3837opreq1d 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))
408, 2, 39mp2an 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))
4230, 3, 7, 41mp3an 919 . . . . . . . . . . . . . . . 16 |- (-uA / (1 - A)) = ((1 / (1 - A)) x. -uA)
4340, 42eqtr4i 1535 . . . . . . . . . . . . . . 15 |- (-u(1 / (1 - A)) x. A) = (-uA / (1 - A))
4443opreq1i 4047 . . . . . . . . . . . . . 14 |- ((-u(1 / (1 - A)) x. A) x. (F` n)) = ((-uA / (1 - A)) x. (F` n))
4544eqcomi 1516 . . . . . . . . . . . . 13 |- ((-uA / (1 - A)) x. (F` n)) = ((-u(1 / (1 - A)) x. A) x. (F` n))
4645a1i 8 . . . . . . . . . . . 12 |- (n e. NN0 -> ((-uA / (1 - A)) x. (F` n)) = ((-u(1 / (1 - A)) x. A) x. (F` n)))
4734, 38, 463eqtr3d 1552 . . . . . . . . . . 11 |- (n e. NN0 -> (-u(A x. (F` n)) / (1 - A)) = ((-u(1 / (1 - A)) x. A) x. (F` n)))
4829, 47eqtrd 1544 . . . . . . . . . 10 |- (n e. NN0 -> (G` n) = ((-u(1 / (1 - A)) x. A) x. (F` n)))
4928, 48jca 286 . . . . . . . . 9 |- (n e. NN0 -> ((F` n) e. CC /\ (G` n) = ((-u(1 / (1 - A)) x. A) x. (F` n))))
5024, 49sylbir 199 . . . . . . . 8 |- (n e. (ZZ>` 0) -> ((F` n) e. CC /\ (G` n) = ((-u(1 / (1 - A)) x. A) x. (F` n))))
5150rgen 1736 . . . . . . 7 |- A.n e. (ZZ>` 0)((F` n) e. CC /\ (G` n) = ((-u(1 / (1 - A)) x. A) x. (F` n)))
5223, 51pm3.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)
5553, 18, 54mp2an 700 . . . . . . 7 |- G e. V
5623elisseti 1856 . . . . . . 7 |- 0 e. V
5719, 55, 56climmulc2 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))
5822, 52, 57mp2an 700 . . . . 5 |- G ~~> ((-u(1 / (1 - A)) x. A) x. 0)
5910mul01i 5520 . . . . 5 |- ((-u(1 / (1 - A)) x. A) x. 0) = 0
6058, 59breqtri 2688 . . . 4 |- G ~~> 0
6160, 8pm3.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)
632, 62mpan 698 . . . . . . . . . . 11 |- ((F` n) e. CC -> (A x. (F` n)) e. CC)
6428, 63syl 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)
6664, 65syl 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)
683, 7, 67mp3an23 911 . . . . . . . . 9 |- (-u(A x. (F` n)) e. CC -> (-u(A x. (F` n)) / (1 - A)) e. CC)
6966, 68syl 10 . . . . . . . 8 |- (n e. NN0 -> (-u(A x. (F` n)) / (1 - A)) e. CC)
7029, 69eqeltrd 1585 . . . . . . 7 |- (n e. NN0 -> (G` n) e. CC)
71 expcl 6704 . . . . . . . . . . . . . . 15 |- ((A e. CC /\ n e. NN0) -> (A^n) e. CC)
722, 71mpan 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))
742, 73mpan 698 . . . . . . . . . . . . . 14 |- ((A^n) e. CC -> (A x. (A^n)) = ((A^n) x. A)