| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | geolim3.f | . . 3
⊢ 𝐹 = (𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) | 
| 2 |  | seqeq3 14048 | . . 3
⊢ (𝐹 = (𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) → seq𝐴( + , 𝐹) = seq𝐴( + , (𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))))) | 
| 3 | 1, 2 | ax-mp 5 | . 2
⊢ seq𝐴( + , 𝐹) = seq𝐴( + , (𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴))))) | 
| 4 |  | nn0uz 12921 | . . . . 5
⊢
ℕ0 = (ℤ≥‘0) | 
| 5 |  | 0zd 12627 | . . . . 5
⊢ (𝜑 → 0 ∈
ℤ) | 
| 6 |  | geolim3.c | . . . . 5
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 7 |  | geolim3.b1 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 8 |  | geolim3.b2 | . . . . . 6
⊢ (𝜑 → (abs‘𝐵) < 1) | 
| 9 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑘 = 𝑎 → (𝐵↑𝑘) = (𝐵↑𝑎)) | 
| 10 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ (𝐵↑𝑘)) = (𝑘 ∈ ℕ0 ↦ (𝐵↑𝑘)) | 
| 11 |  | ovex 7465 | . . . . . . . 8
⊢ (𝐵↑𝑎) ∈ V | 
| 12 | 9, 10, 11 | fvmpt 7015 | . . . . . . 7
⊢ (𝑎 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (𝐵↑𝑘))‘𝑎) = (𝐵↑𝑎)) | 
| 13 | 12 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (𝐵↑𝑘))‘𝑎) = (𝐵↑𝑎)) | 
| 14 | 7, 8, 13 | geolim 15907 | . . . . 5
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ (𝐵↑𝑘))) ⇝ (1 / (1 −
𝐵))) | 
| 15 |  | expcl 14121 | . . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ 𝑎 ∈ ℕ0)
→ (𝐵↑𝑎) ∈
ℂ) | 
| 16 | 7, 15 | sylan 580 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ0) → (𝐵↑𝑎) ∈ ℂ) | 
| 17 | 13, 16 | eqeltrd 2840 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (𝐵↑𝑘))‘𝑎) ∈ ℂ) | 
| 18 |  | geolim3.a | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℤ) | 
| 19 | 18 | zcnd 12725 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 20 |  | nn0cn 12538 | . . . . . . 7
⊢ (𝑎 ∈ ℕ0
→ 𝑎 ∈
ℂ) | 
| 21 |  | fvex 6918 | . . . . . . . . 9
⊢
(ℤ≥‘𝐴) ∈ V | 
| 22 | 21 | mptex 7244 | . . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) ∈ V | 
| 23 | 22 | shftval4 15117 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (((𝑘 ∈
(ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) shift -𝐴)‘𝑎) = ((𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴))))‘(𝐴 + 𝑎))) | 
| 24 | 19, 20, 23 | syl2an 596 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ0) → (((𝑘 ∈
(ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) shift -𝐴)‘𝑎) = ((𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴))))‘(𝐴 + 𝑎))) | 
| 25 |  | uzid 12894 | . . . . . . . . 9
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
(ℤ≥‘𝐴)) | 
| 26 | 18, 25 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘𝐴)) | 
| 27 |  | uzaddcl 12947 | . . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘𝐴) ∧ 𝑎 ∈ ℕ0) → (𝐴 + 𝑎) ∈ (ℤ≥‘𝐴)) | 
| 28 | 26, 27 | sylan 580 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ0) → (𝐴 + 𝑎) ∈ (ℤ≥‘𝐴)) | 
| 29 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑘 = (𝐴 + 𝑎) → (𝑘 − 𝐴) = ((𝐴 + 𝑎) − 𝐴)) | 
| 30 | 29 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑘 = (𝐴 + 𝑎) → (𝐵↑(𝑘 − 𝐴)) = (𝐵↑((𝐴 + 𝑎) − 𝐴))) | 
| 31 | 30 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑘 = (𝐴 + 𝑎) → (𝐶 · (𝐵↑(𝑘 − 𝐴))) = (𝐶 · (𝐵↑((𝐴 + 𝑎) − 𝐴)))) | 
| 32 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) = (𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) | 
| 33 |  | ovex 7465 | . . . . . . . 8
⊢ (𝐶 · (𝐵↑((𝐴 + 𝑎) − 𝐴))) ∈ V | 
| 34 | 31, 32, 33 | fvmpt 7015 | . . . . . . 7
⊢ ((𝐴 + 𝑎) ∈ (ℤ≥‘𝐴) → ((𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴))))‘(𝐴 + 𝑎)) = (𝐶 · (𝐵↑((𝐴 + 𝑎) − 𝐴)))) | 
| 35 | 28, 34 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ0) → ((𝑘 ∈
(ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴))))‘(𝐴 + 𝑎)) = (𝐶 · (𝐵↑((𝐴 + 𝑎) − 𝐴)))) | 
| 36 |  | pncan2 11516 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑎 ∈ ℂ) → ((𝐴 + 𝑎) − 𝐴) = 𝑎) | 
| 37 | 19, 20, 36 | syl2an 596 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ0) → ((𝐴 + 𝑎) − 𝐴) = 𝑎) | 
| 38 | 37 | oveq2d 7448 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ0) → (𝐵↑((𝐴 + 𝑎) − 𝐴)) = (𝐵↑𝑎)) | 
| 39 | 38, 13 | eqtr4d 2779 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ0) → (𝐵↑((𝐴 + 𝑎) − 𝐴)) = ((𝑘 ∈ ℕ0 ↦ (𝐵↑𝑘))‘𝑎)) | 
| 40 | 39 | oveq2d 7448 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ0) → (𝐶 · (𝐵↑((𝐴 + 𝑎) − 𝐴))) = (𝐶 · ((𝑘 ∈ ℕ0 ↦ (𝐵↑𝑘))‘𝑎))) | 
| 41 | 24, 35, 40 | 3eqtrd 2780 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ℕ0) → (((𝑘 ∈
(ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) shift -𝐴)‘𝑎) = (𝐶 · ((𝑘 ∈ ℕ0 ↦ (𝐵↑𝑘))‘𝑎))) | 
| 42 | 4, 5, 6, 14, 17, 41 | isermulc2 15695 | . . . 4
⊢ (𝜑 → seq0( + , ((𝑘 ∈
(ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) shift -𝐴)) ⇝ (𝐶 · (1 / (1 − 𝐵)))) | 
| 43 | 19 | negidd 11611 | . . . . 5
⊢ (𝜑 → (𝐴 + -𝐴) = 0) | 
| 44 | 43 | seqeq1d 14049 | . . . 4
⊢ (𝜑 → seq(𝐴 + -𝐴)( + , ((𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) shift -𝐴)) = seq0( + , ((𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) shift -𝐴))) | 
| 45 |  | ax-1cn 11214 | . . . . . 6
⊢ 1 ∈
ℂ | 
| 46 |  | subcl 11508 | . . . . . 6
⊢ ((1
∈ ℂ ∧ 𝐵
∈ ℂ) → (1 − 𝐵) ∈ ℂ) | 
| 47 | 45, 7, 46 | sylancr 587 | . . . . 5
⊢ (𝜑 → (1 − 𝐵) ∈
ℂ) | 
| 48 |  | abs1 15337 | . . . . . . . . 9
⊢
(abs‘1) = 1 | 
| 49 | 48 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (abs‘1) =
1) | 
| 50 | 7 | abscld 15476 | . . . . . . . . 9
⊢ (𝜑 → (abs‘𝐵) ∈
ℝ) | 
| 51 | 50, 8 | gtned 11397 | . . . . . . . 8
⊢ (𝜑 → 1 ≠ (abs‘𝐵)) | 
| 52 | 49, 51 | eqnetrd 3007 | . . . . . . 7
⊢ (𝜑 → (abs‘1) ≠
(abs‘𝐵)) | 
| 53 |  | fveq2 6905 | . . . . . . . 8
⊢ (1 =
𝐵 → (abs‘1) =
(abs‘𝐵)) | 
| 54 | 53 | necon3i 2972 | . . . . . . 7
⊢
((abs‘1) ≠ (abs‘𝐵) → 1 ≠ 𝐵) | 
| 55 | 52, 54 | syl 17 | . . . . . 6
⊢ (𝜑 → 1 ≠ 𝐵) | 
| 56 |  | subeq0 11536 | . . . . . . . 8
⊢ ((1
∈ ℂ ∧ 𝐵
∈ ℂ) → ((1 − 𝐵) = 0 ↔ 1 = 𝐵)) | 
| 57 | 45, 7, 56 | sylancr 587 | . . . . . . 7
⊢ (𝜑 → ((1 − 𝐵) = 0 ↔ 1 = 𝐵)) | 
| 58 | 57 | necon3bid 2984 | . . . . . 6
⊢ (𝜑 → ((1 − 𝐵) ≠ 0 ↔ 1 ≠ 𝐵)) | 
| 59 | 55, 58 | mpbird 257 | . . . . 5
⊢ (𝜑 → (1 − 𝐵) ≠ 0) | 
| 60 | 6, 47, 59 | divrecd 12047 | . . . 4
⊢ (𝜑 → (𝐶 / (1 − 𝐵)) = (𝐶 · (1 / (1 − 𝐵)))) | 
| 61 | 42, 44, 60 | 3brtr4d 5174 | . . 3
⊢ (𝜑 → seq(𝐴 + -𝐴)( + , ((𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) shift -𝐴)) ⇝ (𝐶 / (1 − 𝐵))) | 
| 62 | 18 | znegcld 12726 | . . . 4
⊢ (𝜑 → -𝐴 ∈ ℤ) | 
| 63 | 22 | isershft 15701 | . . . 4
⊢ ((𝐴 ∈ ℤ ∧ -𝐴 ∈ ℤ) →
(seq𝐴( + , (𝑘 ∈
(ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴))))) ⇝ (𝐶 / (1 − 𝐵)) ↔ seq(𝐴 + -𝐴)( + , ((𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) shift -𝐴)) ⇝ (𝐶 / (1 − 𝐵)))) | 
| 64 | 18, 62, 63 | syl2anc 584 | . . 3
⊢ (𝜑 → (seq𝐴( + , (𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴))))) ⇝ (𝐶 / (1 − 𝐵)) ↔ seq(𝐴 + -𝐴)( + , ((𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴)))) shift -𝐴)) ⇝ (𝐶 / (1 − 𝐵)))) | 
| 65 | 61, 64 | mpbird 257 | . 2
⊢ (𝜑 → seq𝐴( + , (𝑘 ∈ (ℤ≥‘𝐴) ↦ (𝐶 · (𝐵↑(𝑘 − 𝐴))))) ⇝ (𝐶 / (1 − 𝐵))) | 
| 66 | 3, 65 | eqbrtrid 5177 | 1
⊢ (𝜑 → seq𝐴( + , 𝐹) ⇝ (𝐶 / (1 − 𝐵))) |