Metamath Proof Explorer

Theorem georeclim

Description: The limit of a geometric series of reciprocals. (Contributed by Paul Chapman, 28-Dec-2007) (Revised by Mario Carneiro, 26-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 georeclim.1 ${⊢}{\phi }\to {A}\in ℂ$
2 georeclim.2 ${⊢}{\phi }\to 1<\left|{A}\right|$
3 georeclim.3 ${⊢}\left({\phi }\wedge {k}\in {ℕ}_{0}\right)\to {F}\left({k}\right)={\left(\frac{1}{{A}}\right)}^{{k}}$
4 0le1 ${⊢}0\le 1$
5 0re ${⊢}0\in ℝ$
6 1re ${⊢}1\in ℝ$
7 5 6 lenlti ${⊢}0\le 1↔¬1<0$
8 4 7 mpbi ${⊢}¬1<0$
9 fveq2 ${⊢}{A}=0\to \left|{A}\right|=\left|0\right|$
10 abs0 ${⊢}\left|0\right|=0$
11 9 10 syl6eq ${⊢}{A}=0\to \left|{A}\right|=0$
12 11 breq2d ${⊢}{A}=0\to \left(1<\left|{A}\right|↔1<0\right)$
13 8 12 mtbiri ${⊢}{A}=0\to ¬1<\left|{A}\right|$
14 13 necon2ai ${⊢}1<\left|{A}\right|\to {A}\ne 0$
15 2 14 syl ${⊢}{\phi }\to {A}\ne 0$
16 1 15 reccld ${⊢}{\phi }\to \frac{1}{{A}}\in ℂ$
17 1cnd ${⊢}{\phi }\to 1\in ℂ$
18 17 1 15 absdivd ${⊢}{\phi }\to \left|\frac{1}{{A}}\right|=\frac{\left|1\right|}{\left|{A}\right|}$
19 abs1 ${⊢}\left|1\right|=1$
20 19 oveq1i ${⊢}\frac{\left|1\right|}{\left|{A}\right|}=\frac{1}{\left|{A}\right|}$
21 18 20 syl6eq ${⊢}{\phi }\to \left|\frac{1}{{A}}\right|=\frac{1}{\left|{A}\right|}$
22 1 15 absrpcld ${⊢}{\phi }\to \left|{A}\right|\in {ℝ}^{+}$
23 22 recgt1d ${⊢}{\phi }\to \left(1<\left|{A}\right|↔\frac{1}{\left|{A}\right|}<1\right)$
24 2 23 mpbid ${⊢}{\phi }\to \frac{1}{\left|{A}\right|}<1$
25 21 24 eqbrtrd ${⊢}{\phi }\to \left|\frac{1}{{A}}\right|<1$
26 16 25 3 geolim ${⊢}{\phi }\to seq0\left(+,{F}\right)⇝\left(\frac{1}{1-\left(\frac{1}{{A}}\right)}\right)$
27 1 17 1 15 divsubdird ${⊢}{\phi }\to \frac{{A}-1}{{A}}=\left(\frac{{A}}{{A}}\right)-\left(\frac{1}{{A}}\right)$
28 1 15 dividd ${⊢}{\phi }\to \frac{{A}}{{A}}=1$
29 28 oveq1d ${⊢}{\phi }\to \left(\frac{{A}}{{A}}\right)-\left(\frac{1}{{A}}\right)=1-\left(\frac{1}{{A}}\right)$
30 27 29 eqtrd ${⊢}{\phi }\to \frac{{A}-1}{{A}}=1-\left(\frac{1}{{A}}\right)$
31 30 oveq2d ${⊢}{\phi }\to \frac{1}{\frac{{A}-1}{{A}}}=\frac{1}{1-\left(\frac{1}{{A}}\right)}$
32 ax-1cn ${⊢}1\in ℂ$
33 subcl ${⊢}\left({A}\in ℂ\wedge 1\in ℂ\right)\to {A}-1\in ℂ$
34 1 32 33 sylancl ${⊢}{\phi }\to {A}-1\in ℂ$
35 6 ltnri ${⊢}¬1<1$
36 fveq2 ${⊢}{A}=1\to \left|{A}\right|=\left|1\right|$
37 36 19 syl6eq ${⊢}{A}=1\to \left|{A}\right|=1$
38 37 breq2d ${⊢}{A}=1\to \left(1<\left|{A}\right|↔1<1\right)$
39 35 38 mtbiri ${⊢}{A}=1\to ¬1<\left|{A}\right|$
40 39 necon2ai ${⊢}1<\left|{A}\right|\to {A}\ne 1$
41 2 40 syl ${⊢}{\phi }\to {A}\ne 1$
42 subeq0 ${⊢}\left({A}\in ℂ\wedge 1\in ℂ\right)\to \left({A}-1=0↔{A}=1\right)$
43 1 32 42 sylancl ${⊢}{\phi }\to \left({A}-1=0↔{A}=1\right)$
44 43 necon3bid ${⊢}{\phi }\to \left({A}-1\ne 0↔{A}\ne 1\right)$
45 41 44 mpbird ${⊢}{\phi }\to {A}-1\ne 0$
46 34 1 45 15 recdivd ${⊢}{\phi }\to \frac{1}{\frac{{A}-1}{{A}}}=\frac{{A}}{{A}-1}$
47 31 46 eqtr3d ${⊢}{\phi }\to \frac{1}{1-\left(\frac{1}{{A}}\right)}=\frac{{A}}{{A}-1}$
48 26 47 breqtrd ${⊢}{\phi }\to seq0\left(+,{F}\right)⇝\left(\frac{{A}}{{A}-1}\right)$