This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
geolim.2 ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) < 1 )
geolim.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
Assertion geolim ( 𝜑 → seq 0 ( + , 𝐹 ) ⇝ ( 1 / ( 1 − 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 geolim.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 geolim.2 ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) < 1 )
3 geolim.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
4 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
5 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
6 1 2 expcnv ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ⇝ 0 )
7 ax-1cn ⊢ 1 ∈ ℂ
8 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 − 𝐴 ) ∈ ℂ )
9 7 1 8 sylancr ⊢ ( 𝜑 → ( 1 − 𝐴 ) ∈ ℂ )
10 1re ⊢ 1 ∈ ℝ
11 10 ltnri ⊢ ¬ 1 < 1
12 fveq2 ⊢ ( 𝐴 = 1 → ( abs ‘ 𝐴 ) = ( abs ‘ 1 ) )
13 abs1 ⊢ ( abs ‘ 1 ) = 1
14 12 13 eqtrdi ⊢ ( 𝐴 = 1 → ( abs ‘ 𝐴 ) = 1 )
15 14 breq1d ⊢ ( 𝐴 = 1 → ( ( abs ‘ 𝐴 ) < 1 ↔ 1 < 1 ) )
16 11 15 mtbiri ⊢ ( 𝐴 = 1 → ¬ ( abs ‘ 𝐴 ) < 1 )
17 16 necon2ai ⊢ ( ( abs ‘ 𝐴 ) < 1 → 𝐴 ≠ 1 )
18 2 17 syl ⊢ ( 𝜑 → 𝐴 ≠ 1 )
19 18 necomd ⊢ ( 𝜑 → 1 ≠ 𝐴 )
20 subeq0 ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
21 7 1 20 sylancr ⊢ ( 𝜑 → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
22 21 necon3bid ⊢ ( 𝜑 → ( ( 1 − 𝐴 ) ≠ 0 ↔ 1 ≠ 𝐴 ) )
23 19 22 mpbird ⊢ ( 𝜑 → ( 1 − 𝐴 ) ≠ 0 )
24 1 9 23 divcld ⊢ ( 𝜑 → ( 𝐴 / ( 1 − 𝐴 ) ) ∈ ℂ )
25 nn0ex ⊢ ℕ0 ∈ V
26 25 mptex ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ∈ V
27 26 a1i ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ∈ V )
28 oveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑗 ) )
29 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) )
30 ovex ⊢ ( 𝐴 ↑ 𝑗 ) ∈ V
31 28 29 30 fvmpt ⊢ ( 𝑗 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑗 ) = ( 𝐴 ↑ 𝑗 ) )
32 31 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑗 ) = ( 𝐴 ↑ 𝑗 ) )
33 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑗 ) ∈ ℂ )
34 1 33 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑗 ) ∈ ℂ )
35 32 34 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑗 ) ∈ ℂ )
36 expp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑗 + 1 ) ) = ( ( 𝐴 ↑ 𝑗 ) · 𝐴 ) )
37 1 36 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑗 + 1 ) ) = ( ( 𝐴 ↑ 𝑗 ) · 𝐴 ) )
38 1 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
39 34 38 mulcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑗 ) · 𝐴 ) = ( 𝐴 · ( 𝐴 ↑ 𝑗 ) ) )
40 37 39 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑗 + 1 ) ) = ( 𝐴 · ( 𝐴 ↑ 𝑗 ) ) )
41 40 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) = ( ( 𝐴 · ( 𝐴 ↑ 𝑗 ) ) / ( 1 − 𝐴 ) ) )
42 9 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 1 − 𝐴 ) ∈ ℂ )
43 23 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 1 − 𝐴 ) ≠ 0 )
44 38 34 42 43 div23d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 · ( 𝐴 ↑ 𝑗 ) ) / ( 1 − 𝐴 ) ) = ( ( 𝐴 / ( 1 − 𝐴 ) ) · ( 𝐴 ↑ 𝑗 ) ) )
45 41 44 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) = ( ( 𝐴 / ( 1 − 𝐴 ) ) · ( 𝐴 ↑ 𝑗 ) ) )
46 oveq1 ⊢ ( 𝑛 = 𝑗 → ( 𝑛 + 1 ) = ( 𝑗 + 1 ) )
47 46 oveq2d ⊢ ( 𝑛 = 𝑗 → ( 𝐴 ↑ ( 𝑛 + 1 ) ) = ( 𝐴 ↑ ( 𝑗 + 1 ) ) )
48 47 oveq1d ⊢ ( 𝑛 = 𝑗 → ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) = ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) )
49 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) )
50 ovex ⊢ ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) ∈ V
51 48 49 50 fvmpt ⊢ ( 𝑗 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ‘ 𝑗 ) = ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) )
52 51 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ‘ 𝑗 ) = ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) )
53 32 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 / ( 1 − 𝐴 ) ) · ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑗 ) ) = ( ( 𝐴 / ( 1 − 𝐴 ) ) · ( 𝐴 ↑ 𝑗 ) ) )
54 45 52 53 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ‘ 𝑗 ) = ( ( 𝐴 / ( 1 − 𝐴 ) ) · ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑗 ) ) )
55 4 5 6 24 27 35 54 climmulc2 ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ⇝ ( ( 𝐴 / ( 1 − 𝐴 ) ) · 0 ) )
56 24 mul01d ⊢ ( 𝜑 → ( ( 𝐴 / ( 1 − 𝐴 ) ) · 0 ) = 0 )
57 55 56 breqtrd ⊢ ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ⇝ 0 )
58 9 23 reccld ⊢ ( 𝜑 → ( 1 / ( 1 − 𝐴 ) ) ∈ ℂ )
59 seqex ⊢ seq 0 ( + , 𝐹 ) ∈ V
60 59 a1i ⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ∈ V )
61 peano2nn0 ⊢ ( 𝑗 ∈ ℕ0 → ( 𝑗 + 1 ) ∈ ℕ0 )
62 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑗 + 1 ) ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑗 + 1 ) ) ∈ ℂ )
63 1 61 62 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑗 + 1 ) ) ∈ ℂ )
64 63 42 43 divcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) ∈ ℂ )
65 52 64 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ‘ 𝑗 ) ∈ ℂ )
66 nn0cn ⊢ ( 𝑗 ∈ ℕ0 → 𝑗 ∈ ℂ )
67 66 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℂ )
68 pncan ⊢ ( ( 𝑗 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑗 + 1 ) − 1 ) = 𝑗 )
69 67 7 68 sylancl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑗 + 1 ) − 1 ) = 𝑗 )
70 69 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 0 ... ( ( 𝑗 + 1 ) − 1 ) ) = ( 0 ... 𝑗 ) )
71 70 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... ( ( 𝑗 + 1 ) − 1 ) ) ( 𝐴 ↑ 𝑘 ) = Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( 𝐴 ↑ 𝑘 ) )
72 7 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 1 ∈ ℂ )
73 72 63 42 43 divsubdird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 1 − ( 𝐴 ↑ ( 𝑗 + 1 ) ) ) / ( 1 − 𝐴 ) ) = ( ( 1 / ( 1 − 𝐴 ) ) − ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) ) )
74 18 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝐴 ≠ 1 )
75 61 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝑗 + 1 ) ∈ ℕ0 )
76 38 74 75 geoser ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... ( ( 𝑗 + 1 ) − 1 ) ) ( 𝐴 ↑ 𝑘 ) = ( ( 1 − ( 𝐴 ↑ ( 𝑗 + 1 ) ) ) / ( 1 − 𝐴 ) ) )
77 52 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 1 / ( 1 − 𝐴 ) ) − ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ‘ 𝑗 ) ) = ( ( 1 / ( 1 − 𝐴 ) ) − ( ( 𝐴 ↑ ( 𝑗 + 1 ) ) / ( 1 − 𝐴 ) ) ) )
78 73 76 77 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... ( ( 𝑗 + 1 ) − 1 ) ) ( 𝐴 ↑ 𝑘 ) = ( ( 1 / ( 1 − 𝐴 ) ) − ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ‘ 𝑗 ) ) )
79 simpll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → 𝜑 )
80 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑗 ) → 𝑘 ∈ ℕ0 )
81 80 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → 𝑘 ∈ ℕ0 )
82 79 81 3 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
83 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℕ0 )
84 83 4 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ( ℤ≥ ‘ 0 ) )
85 79 1 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → 𝐴 ∈ ℂ )
86 85 81 expcld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑗 ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
87 82 84 86 fsumser ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝑗 ) ( 𝐴 ↑ 𝑘 ) = ( seq 0 ( + , 𝐹 ) ‘ 𝑗 ) )
88 71 78 87 3eqtr3rd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( seq 0 ( + , 𝐹 ) ‘ 𝑗 ) = ( ( 1 / ( 1 − 𝐴 ) ) − ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ ( 𝑛 + 1 ) ) / ( 1 − 𝐴 ) ) ) ‘ 𝑗 ) ) )
89 4 5 57 58 60 65 88 climsubc2 ⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ⇝ ( ( 1 / ( 1 − 𝐴 ) ) − 0 ) )
90 58 subid1d ⊢ ( 𝜑 → ( ( 1 / ( 1 − 𝐴 ) ) − 0 ) = ( 1 / ( 1 − 𝐴 ) ) )
91 89 90 breqtrd ⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ⇝ ( 1 / ( 1 − 𝐴 ) ) )