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 − 𝐴 ) ) )