Metamath Proof Explorer

Theorem geolim2

Description: The partial sums in the geometric series A ^ M + A ^ ( M + 1 ) ... converge to ( ( A ^ M ) / ( 1 - A ) ) . (Contributed by NM, 6-Jun-2006) (Revised by Mario Carneiro, 26-Apr-2014)

Ref Expression
Hypotheses geolim.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
geolim.2 ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) < 1 )
geolim2.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
geolim2.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
Assertion geolim2 ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( ( 𝐴 ↑ 𝑀 ) / ( 1 − 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 geolim.1 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 geolim.2 ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) < 1 )
3 geolim2.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
4 geolim2.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
5 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
6 3 nn0zd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
7 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 ∈ ℂ )
8 eluznn0 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ0 )
9 3 8 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ0 )
10 7 9 expcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
11 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑘 ) )
12 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) )
13 ovex ⊢ ( 𝐴 ↑ 𝑘 ) ∈ V
14 11 12 13 fvmpt ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
15 9 14 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
16 15 4 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
17 6 16 seqfeq ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) = seq 𝑀 ( + , 𝐹 ) )
18 oveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑗 ) )
19 ovex ⊢ ( 𝐴 ↑ 𝑗 ) ∈ V
20 18 12 19 fvmpt ⊢ ( 𝑗 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑗 ) = ( 𝐴 ↑ 𝑗 ) )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑗 ) = ( 𝐴 ↑ 𝑗 ) )
22 1 2 21 geolim ⊢ ( 𝜑 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) ⇝ ( 1 / ( 1 − 𝐴 ) ) )
23 seqex ⊢ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) ∈ V
24 ovex ⊢ ( 1 / ( 1 − 𝐴 ) ) ∈ V
25 23 24 breldm ⊢ ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) ⇝ ( 1 / ( 1 − 𝐴 ) ) → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) ∈ dom ⇝ )
26 22 25 syl ⊢ ( 𝜑 → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) ∈ dom ⇝ )
27 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
28 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑗 ) ∈ ℂ )
29 1 28 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑗 ) ∈ ℂ )
30 21 29 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑗 ) ∈ ℂ )
31 27 3 30 iserex ⊢ ( 𝜑 → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) ∈ dom ⇝ ↔ seq 𝑀 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) ∈ dom ⇝ ) )
32 26 31 mpbid ⊢ ( 𝜑 → seq 𝑀 ( + , ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ) ∈ dom ⇝ )
33 17 32 eqeltrrd ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
34 5 6 4 10 33 isumclim2 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐴 ↑ 𝑘 ) )
35 14 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( 𝐴 ↑ 𝑛 ) ) ‘ 𝑘 ) = ( 𝐴 ↑ 𝑘 ) )
36 expcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
37 1 36 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
38 27 5 3 35 37 26 isumsplit ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 ( 𝐴 ↑ 𝑘 ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( 𝐴 ↑ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐴 ↑ 𝑘 ) ) )
39 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
40 27 39 35 37 22 isumclim ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 ( 𝐴 ↑ 𝑘 ) = ( 1 / ( 1 − 𝐴 ) ) )
41 38 40 eqtr3d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( 𝐴 ↑ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐴 ↑ 𝑘 ) ) = ( 1 / ( 1 − 𝐴 ) ) )
42 1re ⊢ 1 ∈ ℝ
43 42 ltnri ⊢ ¬ 1 < 1
44 fveq2 ⊢ ( 𝐴 = 1 → ( abs ‘ 𝐴 ) = ( abs ‘ 1 ) )
45 abs1 ⊢ ( abs ‘ 1 ) = 1
46 44 45 eqtrdi ⊢ ( 𝐴 = 1 → ( abs ‘ 𝐴 ) = 1 )
47 46 breq1d ⊢ ( 𝐴 = 1 → ( ( abs ‘ 𝐴 ) < 1 ↔ 1 < 1 ) )
48 43 47 mtbiri ⊢ ( 𝐴 = 1 → ¬ ( abs ‘ 𝐴 ) < 1 )
49 48 necon2ai ⊢ ( ( abs ‘ 𝐴 ) < 1 → 𝐴 ≠ 1 )
50 2 49 syl ⊢ ( 𝜑 → 𝐴 ≠ 1 )
51 1 50 3 geoser ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( 𝐴 ↑ 𝑘 ) = ( ( 1 − ( 𝐴 ↑ 𝑀 ) ) / ( 1 − 𝐴 ) ) )
52 51 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( 𝐴 ↑ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐴 ↑ 𝑘 ) ) = ( ( ( 1 − ( 𝐴 ↑ 𝑀 ) ) / ( 1 − 𝐴 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐴 ↑ 𝑘 ) ) )
53 41 52 eqtr3d ⊢ ( 𝜑 → ( 1 / ( 1 − 𝐴 ) ) = ( ( ( 1 − ( 𝐴 ↑ 𝑀 ) ) / ( 1 − 𝐴 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐴 ↑ 𝑘 ) ) )
54 53 oveq1d ⊢ ( 𝜑 → ( ( 1 / ( 1 − 𝐴 ) ) − ( ( 1 − ( 𝐴 ↑ 𝑀 ) ) / ( 1 − 𝐴 ) ) ) = ( ( ( ( 1 − ( 𝐴 ↑ 𝑀 ) ) / ( 1 − 𝐴 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐴 ↑ 𝑘 ) ) − ( ( 1 − ( 𝐴 ↑ 𝑀 ) ) / ( 1 − 𝐴 ) ) ) )
55 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
56 ax-1cn ⊢ 1 ∈ ℂ
57 1 3 expcld ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑀 ) ∈ ℂ )
58 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 𝑀 ) ∈ ℂ ) → ( 1 − ( 𝐴 ↑ 𝑀 ) ) ∈ ℂ )
59 56 57 58 sylancr ⊢ ( 𝜑 → ( 1 − ( 𝐴 ↑ 𝑀 ) ) ∈ ℂ )
60 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 − 𝐴 ) ∈ ℂ )
61 56 1 60 sylancr ⊢ ( 𝜑 → ( 1 − 𝐴 ) ∈ ℂ )
62 50 necomd ⊢ ( 𝜑 → 1 ≠ 𝐴 )
63 subeq0 ⊢ ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
64 56 1 63 sylancr ⊢ ( 𝜑 → ( ( 1 − 𝐴 ) = 0 ↔ 1 = 𝐴 ) )
65 64 necon3bid ⊢ ( 𝜑 → ( ( 1 − 𝐴 ) ≠ 0 ↔ 1 ≠ 𝐴 ) )
66 62 65 mpbird ⊢ ( 𝜑 → ( 1 − 𝐴 ) ≠ 0 )
67 55 59 61 66 divsubdird ⊢ ( 𝜑 → ( ( 1 − ( 1 − ( 𝐴 ↑ 𝑀 ) ) ) / ( 1 − 𝐴 ) ) = ( ( 1 / ( 1 − 𝐴 ) ) − ( ( 1 − ( 𝐴 ↑ 𝑀 ) ) / ( 1 − 𝐴 ) ) ) )
68 nncan ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 𝑀 ) ∈ ℂ ) → ( 1 − ( 1 − ( 𝐴 ↑ 𝑀 ) ) ) = ( 𝐴 ↑ 𝑀 ) )
69 56 57 68 sylancr ⊢ ( 𝜑 → ( 1 − ( 1 − ( 𝐴 ↑ 𝑀 ) ) ) = ( 𝐴 ↑ 𝑀 ) )
70 69 oveq1d ⊢ ( 𝜑 → ( ( 1 − ( 1 − ( 𝐴 ↑ 𝑀 ) ) ) / ( 1 − 𝐴 ) ) = ( ( 𝐴 ↑ 𝑀 ) / ( 1 − 𝐴 ) ) )
71 67 70 eqtr3d ⊢ ( 𝜑 → ( ( 1 / ( 1 − 𝐴 ) ) − ( ( 1 − ( 𝐴 ↑ 𝑀 ) ) / ( 1 − 𝐴 ) ) ) = ( ( 𝐴 ↑ 𝑀 ) / ( 1 − 𝐴 ) ) )
72 59 61 66 divcld ⊢ ( 𝜑 → ( ( 1 − ( 𝐴 ↑ 𝑀 ) ) / ( 1 − 𝐴 ) ) ∈ ℂ )
73 5 6 15 10 32 isumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
74 72 73 pncan2d ⊢ ( 𝜑 → ( ( ( ( 1 − ( 𝐴 ↑ 𝑀 ) ) / ( 1 − 𝐴 ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐴 ↑ 𝑘 ) ) − ( ( 1 − ( 𝐴 ↑ 𝑀 ) ) / ( 1 − 𝐴 ) ) ) = Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐴 ↑ 𝑘 ) )
75 54 71 74 3eqtr3rd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐴 ↑ 𝑘 ) = ( ( 𝐴 ↑ 𝑀 ) / ( 1 − 𝐴 ) ) )
76 34 75 breqtrd ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( ( 𝐴 ↑ 𝑀 ) / ( 1 − 𝐴 ) ) )