| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | addcl 11237 | . . . . 5
⊢ ((𝑛 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑛 + 𝑥) ∈ ℂ) | 
| 2 | 1 | adantl 481 | . . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑛 + 𝑥) ∈ ℂ) | 
| 3 |  | simpll 767 | . . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝜑) | 
| 4 |  | elfznn 13593 | . . . . . 6
⊢ (𝑛 ∈ (1...𝑘) → 𝑛 ∈ ℕ) | 
| 5 | 4 | adantl 481 | . . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → 𝑛 ∈ ℕ) | 
| 6 |  | oveq1 7438 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1)) | 
| 7 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → 𝑚 = 𝑛) | 
| 8 | 6, 7 | oveq12d 7449 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((𝑚 + 1) / 𝑚) = ((𝑛 + 1) / 𝑛)) | 
| 9 | 8 | fveq2d 6910 | . . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑛 + 1) / 𝑛))) | 
| 10 | 9 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝐴 · (log‘((𝑚 + 1) / 𝑚))) = (𝐴 · (log‘((𝑛 + 1) / 𝑛)))) | 
| 11 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → (𝐴 / 𝑚) = (𝐴 / 𝑛)) | 
| 12 | 11 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝑚 = 𝑛 → ((𝐴 / 𝑚) + 1) = ((𝐴 / 𝑛) + 1)) | 
| 13 | 12 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝑚 = 𝑛 → (log‘((𝐴 / 𝑚) + 1)) = (log‘((𝐴 / 𝑛) + 1))) | 
| 14 | 10, 13 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))) = ((𝐴 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝐴 / 𝑛) + 1)))) | 
| 15 |  | gamcvg2.g | . . . . . . . 8
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))) | 
| 16 |  | ovex 7464 | . . . . . . . 8
⊢ ((𝐴 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝐴 / 𝑛) + 1))) ∈ V | 
| 17 | 14, 15, 16 | fvmpt 7016 | . . . . . . 7
⊢ (𝑛 ∈ ℕ → (𝐺‘𝑛) = ((𝐴 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝐴 / 𝑛) + 1)))) | 
| 18 | 17 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = ((𝐴 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝐴 / 𝑛) + 1)))) | 
| 19 |  | gamcvg2.a | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) | 
| 20 | 19 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ (ℂ ∖ (ℤ ∖
ℕ))) | 
| 21 | 20 | eldifad 3963 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ ℂ) | 
| 22 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) | 
| 23 | 22 | peano2nnd 12283 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) | 
| 24 | 23 | nnrpd 13075 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈
ℝ+) | 
| 25 | 22 | nnrpd 13075 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+) | 
| 26 | 24, 25 | rpdivcld 13094 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 + 1) / 𝑛) ∈
ℝ+) | 
| 27 | 26 | relogcld 26665 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝑛 + 1) / 𝑛)) ∈ ℝ) | 
| 28 | 27 | recnd 11289 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝑛 + 1) / 𝑛)) ∈ ℂ) | 
| 29 | 21, 28 | mulcld 11281 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 · (log‘((𝑛 + 1) / 𝑛))) ∈ ℂ) | 
| 30 | 22 | nncnd 12282 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) | 
| 31 | 22 | nnne0d 12316 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0) | 
| 32 | 21, 30, 31 | divcld 12043 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴 / 𝑛) ∈ ℂ) | 
| 33 |  | 1cnd 11256 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 1 ∈
ℂ) | 
| 34 | 32, 33 | addcld 11280 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 / 𝑛) + 1) ∈ ℂ) | 
| 35 | 20, 22 | dmgmdivn0 27071 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 / 𝑛) + 1) ≠ 0) | 
| 36 | 34, 35 | logcld 26612 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝐴 / 𝑛) + 1)) ∈ ℂ) | 
| 37 | 29, 36 | subcld 11620 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝐴 / 𝑛) + 1))) ∈ ℂ) | 
| 38 | 18, 37 | eqeltrd 2841 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) ∈ ℂ) | 
| 39 | 3, 5, 38 | syl2anc 584 | . . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (𝐺‘𝑛) ∈ ℂ) | 
| 40 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) | 
| 41 |  | nnuz 12921 | . . . . 5
⊢ ℕ =
(ℤ≥‘1) | 
| 42 | 40, 41 | eleqtrdi 2851 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
(ℤ≥‘1)) | 
| 43 |  | efadd 16130 | . . . . 5
⊢ ((𝑛 ∈ ℂ ∧ 𝑥 ∈ ℂ) →
(exp‘(𝑛 + 𝑥)) = ((exp‘𝑛) · (exp‘𝑥))) | 
| 44 | 43 | adantl 481 | . . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (𝑛 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (exp‘(𝑛 + 𝑥)) = ((exp‘𝑛) · (exp‘𝑥))) | 
| 45 |  | efsub 16136 | . . . . . . . 8
⊢ (((𝐴 · (log‘((𝑛 + 1) / 𝑛))) ∈ ℂ ∧ (log‘((𝐴 / 𝑛) + 1)) ∈ ℂ) →
(exp‘((𝐴 ·
(log‘((𝑛 + 1) / 𝑛))) − (log‘((𝐴 / 𝑛) + 1)))) = ((exp‘(𝐴 · (log‘((𝑛 + 1) / 𝑛)))) / (exp‘(log‘((𝐴 / 𝑛) + 1))))) | 
| 46 | 29, 36, 45 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (exp‘((𝐴 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝐴 / 𝑛) + 1)))) = ((exp‘(𝐴 · (log‘((𝑛 + 1) / 𝑛)))) / (exp‘(log‘((𝐴 / 𝑛) + 1))))) | 
| 47 | 30, 33 | addcld 11280 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℂ) | 
| 48 | 47, 30, 31 | divcld 12043 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 + 1) / 𝑛) ∈ ℂ) | 
| 49 | 23 | nnne0d 12316 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ≠ 0) | 
| 50 | 47, 30, 49, 31 | divne0d 12059 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 + 1) / 𝑛) ≠ 0) | 
| 51 | 48, 50, 21 | cxpefd 26754 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑛 + 1) / 𝑛)↑𝑐𝐴) = (exp‘(𝐴 · (log‘((𝑛 + 1) / 𝑛))))) | 
| 52 | 51 | eqcomd 2743 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (exp‘(𝐴 · (log‘((𝑛 + 1) / 𝑛)))) = (((𝑛 + 1) / 𝑛)↑𝑐𝐴)) | 
| 53 |  | eflog 26618 | . . . . . . . . 9
⊢ ((((𝐴 / 𝑛) + 1) ∈ ℂ ∧ ((𝐴 / 𝑛) + 1) ≠ 0) →
(exp‘(log‘((𝐴 /
𝑛) + 1))) = ((𝐴 / 𝑛) + 1)) | 
| 54 | 34, 35, 53 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) →
(exp‘(log‘((𝐴 /
𝑛) + 1))) = ((𝐴 / 𝑛) + 1)) | 
| 55 | 52, 54 | oveq12d 7449 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((exp‘(𝐴 · (log‘((𝑛 + 1) / 𝑛)))) / (exp‘(log‘((𝐴 / 𝑛) + 1)))) = ((((𝑛 + 1) / 𝑛)↑𝑐𝐴) / ((𝐴 / 𝑛) + 1))) | 
| 56 | 46, 55 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (exp‘((𝐴 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝐴 / 𝑛) + 1)))) = ((((𝑛 + 1) / 𝑛)↑𝑐𝐴) / ((𝐴 / 𝑛) + 1))) | 
| 57 | 18 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (exp‘(𝐺‘𝑛)) = (exp‘((𝐴 · (log‘((𝑛 + 1) / 𝑛))) − (log‘((𝐴 / 𝑛) + 1))))) | 
| 58 | 8 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝑚 = 𝑛 → (((𝑚 + 1) / 𝑚)↑𝑐𝐴) = (((𝑛 + 1) / 𝑛)↑𝑐𝐴)) | 
| 59 | 58, 12 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑚 = 𝑛 → ((((𝑚 + 1) / 𝑚)↑𝑐𝐴) / ((𝐴 / 𝑚) + 1)) = ((((𝑛 + 1) / 𝑛)↑𝑐𝐴) / ((𝐴 / 𝑛) + 1))) | 
| 60 |  | gamcvg2.f | . . . . . . . 8
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((((𝑚 + 1) / 𝑚)↑𝑐𝐴) / ((𝐴 / 𝑚) + 1))) | 
| 61 |  | ovex 7464 | . . . . . . . 8
⊢ ((((𝑛 + 1) / 𝑛)↑𝑐𝐴) / ((𝐴 / 𝑛) + 1)) ∈ V | 
| 62 | 59, 60, 61 | fvmpt 7016 | . . . . . . 7
⊢ (𝑛 ∈ ℕ → (𝐹‘𝑛) = ((((𝑛 + 1) / 𝑛)↑𝑐𝐴) / ((𝐴 / 𝑛) + 1))) | 
| 63 | 62 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = ((((𝑛 + 1) / 𝑛)↑𝑐𝐴) / ((𝐴 / 𝑛) + 1))) | 
| 64 | 56, 57, 63 | 3eqtr4d 2787 | . . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (exp‘(𝐺‘𝑛)) = (𝐹‘𝑛)) | 
| 65 | 3, 5, 64 | syl2anc 584 | . . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑘)) → (exp‘(𝐺‘𝑛)) = (𝐹‘𝑛)) | 
| 66 | 2, 39, 42, 44, 65 | seqhomo 14090 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (exp‘(seq1( + ,
𝐺)‘𝑘)) = (seq1( · , 𝐹)‘𝑘)) | 
| 67 | 66 | mpteq2dva 5242 | . 2
⊢ (𝜑 → (𝑘 ∈ ℕ ↦ (exp‘(seq1( + ,
𝐺)‘𝑘))) = (𝑘 ∈ ℕ ↦ (seq1( · ,
𝐹)‘𝑘))) | 
| 68 |  | eff 16117 | . . . 4
⊢
exp:ℂ⟶ℂ | 
| 69 | 68 | a1i 11 | . . 3
⊢ (𝜑 →
exp:ℂ⟶ℂ) | 
| 70 |  | 1z 12647 | . . . . 5
⊢ 1 ∈
ℤ | 
| 71 | 70 | a1i 11 | . . . 4
⊢ (𝜑 → 1 ∈
ℤ) | 
| 72 | 41, 71, 38 | serf 14071 | . . 3
⊢ (𝜑 → seq1( + , 𝐺):ℕ⟶ℂ) | 
| 73 |  | fcompt 7153 | . . 3
⊢
((exp:ℂ⟶ℂ ∧ seq1( + , 𝐺):ℕ⟶ℂ) → (exp
∘ seq1( + , 𝐺)) =
(𝑘 ∈ ℕ ↦
(exp‘(seq1( + , 𝐺)‘𝑘)))) | 
| 74 | 69, 72, 73 | syl2anc 584 | . 2
⊢ (𝜑 → (exp ∘ seq1( + ,
𝐺)) = (𝑘 ∈ ℕ ↦ (exp‘(seq1( + ,
𝐺)‘𝑘)))) | 
| 75 |  | seqfn 14054 | . . . . 5
⊢ (1 ∈
ℤ → seq1( · , 𝐹) Fn
(ℤ≥‘1)) | 
| 76 | 70, 75 | mp1i 13 | . . . 4
⊢ (𝜑 → seq1( · , 𝐹) Fn
(ℤ≥‘1)) | 
| 77 | 41 | fneq2i 6666 | . . . 4
⊢ (seq1(
· , 𝐹) Fn ℕ
↔ seq1( · , 𝐹)
Fn (ℤ≥‘1)) | 
| 78 | 76, 77 | sylibr 234 | . . 3
⊢ (𝜑 → seq1( · , 𝐹) Fn ℕ) | 
| 79 |  | dffn5 6967 | . . 3
⊢ (seq1(
· , 𝐹) Fn ℕ
↔ seq1( · , 𝐹)
= (𝑘 ∈ ℕ ↦
(seq1( · , 𝐹)‘𝑘))) | 
| 80 | 78, 79 | sylib 218 | . 2
⊢ (𝜑 → seq1( · , 𝐹) = (𝑘 ∈ ℕ ↦ (seq1( · ,
𝐹)‘𝑘))) | 
| 81 | 67, 74, 80 | 3eqtr4d 2787 | 1
⊢ (𝜑 → (exp ∘ seq1( + ,
𝐺)) = seq1( · ,
𝐹)) |