# Metamath Proof Explorer

## Theorem geolim

Description: The partial sums in the infinite series 1 + A ^ 1 + A ^ 2 ... converge to ( 1 / ( 1 - A ) ) . (Contributed by NM, 15-May-2006)

Ref Expression
Hypotheses geolim.1 ${⊢}{\phi }\to {A}\in ℂ$
geolim.2 ${⊢}{\phi }\to \left|{A}\right|<1$
geolim.3 ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {F}\left({k}\right)={{A}}^{{k}}$
Assertion geolim ${⊢}{\phi }\to seq0\left(+,{F}\right)⇝\left(\frac{1}{1-{A}}\right)$

### Proof

Step Hyp Ref Expression
1 geolim.1 ${⊢}{\phi }\to {A}\in ℂ$
2 geolim.2 ${⊢}{\phi }\to \left|{A}\right|<1$
3 geolim.3 ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {F}\left({k}\right)={{A}}^{{k}}$
4 nn0uz ${⊢}{ℕ}_{0}={ℤ}_{\ge 0}$
5 0zd ${⊢}{\phi }\to 0\in ℤ$
6 1 2 expcnv ${⊢}{\phi }\to \left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)⇝0$
7 ax-1cn ${⊢}1\in ℂ$
8 subcl ${⊢}\left(1\in ℂ\wedge {A}\in ℂ\right)\to 1-{A}\in ℂ$
9 7 1 8 sylancr ${⊢}{\phi }\to 1-{A}\in ℂ$
10 1re ${⊢}1\in ℝ$
11 10 ltnri ${⊢}¬1<1$
12 fveq2 ${⊢}{A}=1\to \left|{A}\right|=\left|1\right|$
13 abs1 ${⊢}\left|1\right|=1$
14 12 13 syl6eq ${⊢}{A}=1\to \left|{A}\right|=1$
15 14 breq1d ${⊢}{A}=1\to \left(\left|{A}\right|<1↔1<1\right)$
16 11 15 mtbiri ${⊢}{A}=1\to ¬\left|{A}\right|<1$
17 16 necon2ai ${⊢}\left|{A}\right|<1\to {A}\ne 1$
18 2 17 syl ${⊢}{\phi }\to {A}\ne 1$
19 18 necomd ${⊢}{\phi }\to 1\ne {A}$
20 subeq0 ${⊢}\left(1\in ℂ\wedge {A}\in ℂ\right)\to \left(1-{A}=0↔1={A}\right)$
21 7 1 20 sylancr ${⊢}{\phi }\to \left(1-{A}=0↔1={A}\right)$
22 21 necon3bid ${⊢}{\phi }\to \left(1-{A}\ne 0↔1\ne {A}\right)$
23 19 22 mpbird ${⊢}{\phi }\to 1-{A}\ne 0$
24 1 9 23 divcld ${⊢}{\phi }\to \frac{{A}}{1-{A}}\in ℂ$
25 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
26 25 mptex ${⊢}\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}+1}}{1-{A}}\right)\in \mathrm{V}$
27 26 a1i ${⊢}{\phi }\to \left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}+1}}{1-{A}}\right)\in \mathrm{V}$
28 oveq2 ${⊢}{n}={j}\to {{A}}^{{n}}={{A}}^{{j}}$
29 eqid ${⊢}\left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)=\left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)$
30 ovex ${⊢}{{A}}^{{j}}\in \mathrm{V}$
31 28 29 30 fvmpt ${⊢}{j}\in {ℕ}_{0}\to \left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)\left({j}\right)={{A}}^{{j}}$
32 31 adantl ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)\left({j}\right)={{A}}^{{j}}$
33 expcl ${⊢}\left({A}\in ℂ\wedge {j}\in {ℕ}_{0}\right)\to {{A}}^{{j}}\in ℂ$
34 1 33 sylan ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {{A}}^{{j}}\in ℂ$
35 32 34 eqeltrd ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)\left({j}\right)\in ℂ$
36 expp1 ${⊢}\left({A}\in ℂ\wedge {j}\in {ℕ}_{0}\right)\to {{A}}^{{j}+1}={{A}}^{{j}}{A}$
37 1 36 sylan ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {{A}}^{{j}+1}={{A}}^{{j}}{A}$
38 1 adantr ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {A}\in ℂ$
39 34 38 mulcomd ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {{A}}^{{j}}{A}={A}{{A}}^{{j}}$
40 37 39 eqtrd ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {{A}}^{{j}+1}={A}{{A}}^{{j}}$
41 40 oveq1d ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \frac{{{A}}^{{j}+1}}{1-{A}}=\frac{{A}{{A}}^{{j}}}{1-{A}}$
42 9 adantr ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to 1-{A}\in ℂ$
43 23 adantr ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to 1-{A}\ne 0$
44 38 34 42 43 div23d ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \frac{{A}{{A}}^{{j}}}{1-{A}}=\left(\frac{{A}}{1-{A}}\right){{A}}^{{j}}$
45 41 44 eqtrd ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \frac{{{A}}^{{j}+1}}{1-{A}}=\left(\frac{{A}}{1-{A}}\right){{A}}^{{j}}$
46 oveq1 ${⊢}{n}={j}\to {n}+1={j}+1$
47 46 oveq2d ${⊢}{n}={j}\to {{A}}^{{n}+1}={{A}}^{{j}+1}$
48 47 oveq1d ${⊢}{n}={j}\to \frac{{{A}}^{{n}+1}}{1-{A}}=\frac{{{A}}^{{j}+1}}{1-{A}}$
49 eqid ${⊢}\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}+1}}{1-{A}}\right)=\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}+1}}{1-{A}}\right)$
50 ovex ${⊢}\frac{{{A}}^{{j}+1}}{1-{A}}\in \mathrm{V}$
51 48 49 50 fvmpt ${⊢}{j}\in {ℕ}_{0}\to \left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}+1}}{1-{A}}\right)\left({j}\right)=\frac{{{A}}^{{j}+1}}{1-{A}}$
52 51 adantl ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}+1}}{1-{A}}\right)\left({j}\right)=\frac{{{A}}^{{j}+1}}{1-{A}}$
53 32 oveq2d ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \left(\frac{{A}}{1-{A}}\right)\left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)\left({j}\right)=\left(\frac{{A}}{1-{A}}\right){{A}}^{{j}}$
54 45 52 53 3eqtr4d ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}+1}}{1-{A}}\right)\left({j}\right)=\left(\frac{{A}}{1-{A}}\right)\left({n}\in {ℕ}_{0}⟼{{A}}^{{n}}\right)\left({j}\right)$
55 4 5 6 24 27 35 54 climmulc2 ${⊢}{\phi }\to \left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}+1}}{1-{A}}\right)⇝\left(\frac{{A}}{1-{A}}\right)\cdot 0$
56 24 mul01d ${⊢}{\phi }\to \left(\frac{{A}}{1-{A}}\right)\cdot 0=0$
57 55 56 breqtrd ${⊢}{\phi }\to \left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}+1}}{1-{A}}\right)⇝0$
58 9 23 reccld ${⊢}{\phi }\to \frac{1}{1-{A}}\in ℂ$
59 seqex ${⊢}seq0\left(+,{F}\right)\in \mathrm{V}$
60 59 a1i ${⊢}{\phi }\to seq0\left(+,{F}\right)\in \mathrm{V}$
61 peano2nn0 ${⊢}{j}\in {ℕ}_{0}\to {j}+1\in {ℕ}_{0}$
62 expcl ${⊢}\left({A}\in ℂ\wedge {j}+1\in {ℕ}_{0}\right)\to {{A}}^{{j}+1}\in ℂ$
63 1 61 62 syl2an ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {{A}}^{{j}+1}\in ℂ$
64 63 42 43 divcld ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \frac{{{A}}^{{j}+1}}{1-{A}}\in ℂ$
65 52 64 eqeltrd ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}+1}}{1-{A}}\right)\left({j}\right)\in ℂ$
66 nn0cn ${⊢}{j}\in {ℕ}_{0}\to {j}\in ℂ$
67 66 adantl ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {j}\in ℂ$
68 pncan ${⊢}\left({j}\in ℂ\wedge 1\in ℂ\right)\to {j}+1-1={j}$
69 67 7 68 sylancl ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {j}+1-1={j}$
70 69 oveq2d ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \left(0\dots {j}+1-1\right)=\left(0\dots {j}\right)$
71 70 sumeq1d ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \sum _{{k}=0}^{{j}+1-1}{{A}}^{{k}}=\sum _{{k}=0}^{{j}}{{A}}^{{k}}$
72 7 a1i ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to 1\in ℂ$
73 72 63 42 43 divsubdird ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \frac{1-{{A}}^{{j}+1}}{1-{A}}=\left(\frac{1}{1-{A}}\right)-\left(\frac{{{A}}^{{j}+1}}{1-{A}}\right)$
74 18 adantr ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {A}\ne 1$
75 61 adantl ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {j}+1\in {ℕ}_{0}$
76 38 74 75 geoser ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \sum _{{k}=0}^{{j}+1-1}{{A}}^{{k}}=\frac{1-{{A}}^{{j}+1}}{1-{A}}$
77 52 oveq2d ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \left(\frac{1}{1-{A}}\right)-\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}+1}}{1-{A}}\right)\left({j}\right)=\left(\frac{1}{1-{A}}\right)-\left(\frac{{{A}}^{{j}+1}}{1-{A}}\right)$
78 73 76 77 3eqtr4d ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \sum _{{k}=0}^{{j}+1-1}{{A}}^{{k}}=\left(\frac{1}{1-{A}}\right)-\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}+1}}{1-{A}}\right)\left({j}\right)$
79 simpll ${⊢}\left(\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {j}\right)\right)\to {\phi }$
80 elfznn0 ${⊢}{k}\in \left(0\dots {j}\right)\to {k}\in {ℕ}_{0}$
81 80 adantl ${⊢}\left(\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {j}\right)\right)\to {k}\in {ℕ}_{0}$
82 79 81 3 syl2anc ${⊢}\left(\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {j}\right)\right)\to {F}\left({k}\right)={{A}}^{{k}}$
83 simpr ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {j}\in {ℕ}_{0}$
84 83 4 eleqtrdi ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to {j}\in {ℤ}_{\ge 0}$
85 79 1 syl ${⊢}\left(\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {j}\right)\right)\to {A}\in ℂ$
86 85 81 expcld ${⊢}\left(\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\wedge {k}\in \left(0\dots {j}\right)\right)\to {{A}}^{{k}}\in ℂ$
87 82 84 86 fsumser ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to \sum _{{k}=0}^{{j}}{{A}}^{{k}}=seq0\left(+,{F}\right)\left({j}\right)$
88 71 78 87 3eqtr3rd ${⊢}\left({\phi }\wedge {j}\in {ℕ}_{0}\right)\to seq0\left(+,{F}\right)\left({j}\right)=\left(\frac{1}{1-{A}}\right)-\left({n}\in {ℕ}_{0}⟼\frac{{{A}}^{{n}+1}}{1-{A}}\right)\left({j}\right)$
89 4 5 57 58 60 65 88 climsubc2 ${⊢}{\phi }\to seq0\left(+,{F}\right)⇝\left(\left(\frac{1}{1-{A}}\right)-0\right)$
90 58 subid1d ${⊢}{\phi }\to \left(\frac{1}{1-{A}}\right)-0=\frac{1}{1-{A}}$
91 89 90 breqtrd ${⊢}{\phi }\to seq0\left(+,{F}\right)⇝\left(\frac{1}{1-{A}}\right)$