| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | abelthlem6.1 | . . . 4
⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1})) | 
| 2 | 1 | eldifad 3962 | . . 3
⊢ (𝜑 → 𝑋 ∈ 𝑆) | 
| 3 |  | oveq1 7439 | . . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥↑𝑛) = (𝑋↑𝑛)) | 
| 4 | 3 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = 𝑋 → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑛) · (𝑋↑𝑛))) | 
| 5 | 4 | sumeq2sdv 15740 | . . . 4
⊢ (𝑥 = 𝑋 → Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑋↑𝑛))) | 
| 6 |  | abelth.6 | . . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) | 
| 7 |  | sumex 15725 | . . . 4
⊢
Σ𝑛 ∈
ℕ0 ((𝐴‘𝑛) · (𝑋↑𝑛)) ∈ V | 
| 8 | 5, 6, 7 | fvmpt 7015 | . . 3
⊢ (𝑋 ∈ 𝑆 → (𝐹‘𝑋) = Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑋↑𝑛))) | 
| 9 | 2, 8 | syl 17 | . 2
⊢ (𝜑 → (𝐹‘𝑋) = Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑋↑𝑛))) | 
| 10 |  | nn0uz 12921 | . . 3
⊢
ℕ0 = (ℤ≥‘0) | 
| 11 |  | 0zd 12627 | . . 3
⊢ (𝜑 → 0 ∈
ℤ) | 
| 12 |  | fveq2 6905 | . . . . . 6
⊢ (𝑘 = 𝑛 → (𝐴‘𝑘) = (𝐴‘𝑛)) | 
| 13 |  | oveq2 7440 | . . . . . 6
⊢ (𝑘 = 𝑛 → (𝑋↑𝑘) = (𝑋↑𝑛)) | 
| 14 | 12, 13 | oveq12d 7450 | . . . . 5
⊢ (𝑘 = 𝑛 → ((𝐴‘𝑘) · (𝑋↑𝑘)) = ((𝐴‘𝑛) · (𝑋↑𝑛))) | 
| 15 |  | eqid 2736 | . . . . 5
⊢ (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑋↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑋↑𝑘))) | 
| 16 |  | ovex 7465 | . . . . 5
⊢ ((𝐴‘𝑛) · (𝑋↑𝑛)) ∈ V | 
| 17 | 14, 15, 16 | fvmpt 7015 | . . . 4
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((𝐴‘𝑛) · (𝑋↑𝑛))) | 
| 18 | 17 | adantl 481 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((𝐴‘𝑛) · (𝑋↑𝑛))) | 
| 19 |  | abelth.1 | . . . . 5
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) | 
| 20 | 19 | ffvelcdmda 7103 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐴‘𝑛) ∈ ℂ) | 
| 21 |  | abelth.5 | . . . . . . 7
⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} | 
| 22 | 21 | ssrab3 4081 | . . . . . 6
⊢ 𝑆 ⊆
ℂ | 
| 23 | 22, 2 | sselid 3980 | . . . . 5
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 24 |  | expcl 14121 | . . . . 5
⊢ ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ (𝑋↑𝑛) ∈
ℂ) | 
| 25 | 23, 24 | sylan 580 | . . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑋↑𝑛) ∈ ℂ) | 
| 26 | 20, 25 | mulcld 11282 | . . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝐴‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) | 
| 27 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑘 = 𝑛 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑛)) | 
| 28 | 27, 13 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑘 = 𝑛 → ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) | 
| 29 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘))) | 
| 30 |  | ovex 7465 | . . . . . . . 8
⊢ ((seq0( +
, 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ V | 
| 31 | 28, 29, 30 | fvmpt 7015 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) | 
| 32 | 31 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) | 
| 33 | 10, 11, 20 | serf 14072 | . . . . . . . 8
⊢ (𝜑 → seq0( + , 𝐴):ℕ0⟶ℂ) | 
| 34 | 33 | ffvelcdmda 7103 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (seq0( +
, 𝐴)‘𝑛) ∈
ℂ) | 
| 35 | 34, 25 | mulcld 11282 | . . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((seq0( +
, 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) | 
| 36 |  | abelth.2 | . . . . . . . . . 10
⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝
) | 
| 37 |  | abelth.3 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 38 |  | abelth.4 | . . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝑀) | 
| 39 | 19, 36, 37, 38, 21 | abelthlem2 26477 | . . . . . . . . 9
⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1))) | 
| 40 | 39 | simprd 495 | . . . . . . . 8
⊢ (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1)) | 
| 41 | 40, 1 | sseldd 3983 | . . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) | 
| 42 |  | abelth.7 | . . . . . . . 8
⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) | 
| 43 | 19, 36, 37, 38, 21, 6, 42 | abelthlem5 26480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → seq0( + , (𝑘
∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ) | 
| 44 | 41, 43 | mpdan 687 | . . . . . 6
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ) | 
| 45 | 10, 11, 32, 35, 44 | isumclim2 15795 | . . . . 5
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ⇝ Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) | 
| 46 |  | seqex 14045 | . . . . . 6
⊢ seq0( + ,
(𝑘 ∈
ℕ0 ↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))) ∈ V | 
| 47 | 46 | a1i 11 | . . . . 5
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))) ∈ V) | 
| 48 |  | 0nn0 12543 | . . . . . . . 8
⊢ 0 ∈
ℕ0 | 
| 49 | 48 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 0 ∈
ℕ0) | 
| 50 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → (𝑘 − 1) = (𝑖 − 1)) | 
| 51 | 50 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → (0...(𝑘 − 1)) = (0...(𝑖 − 1))) | 
| 52 | 51 | sumeq1d 15737 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) = Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴‘𝑚)) | 
| 53 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → (𝑋↑𝑘) = (𝑋↑𝑖)) | 
| 54 | 52, 53 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑘 = 𝑖 → (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)) = (Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴‘𝑚) · (𝑋↑𝑖))) | 
| 55 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))) = (𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))) | 
| 56 |  | ovex 7465 | . . . . . . . . . 10
⊢
(Σ𝑚 ∈
(0...(𝑖 − 1))(𝐴‘𝑚) · (𝑋↑𝑖)) ∈ V | 
| 57 | 54, 55, 56 | fvmpt 7015 | . . . . . . . . 9
⊢ (𝑖 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑖) = (Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴‘𝑚) · (𝑋↑𝑖))) | 
| 58 | 57 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑖) = (Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴‘𝑚) · (𝑋↑𝑖))) | 
| 59 |  | fzfid 14015 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
(0...(𝑖 − 1)) ∈
Fin) | 
| 60 | 19 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝐴:ℕ0⟶ℂ) | 
| 61 |  | elfznn0 13661 | . . . . . . . . . . 11
⊢ (𝑚 ∈ (0...(𝑖 − 1)) → 𝑚 ∈ ℕ0) | 
| 62 |  | ffvelcdm 7100 | . . . . . . . . . . 11
⊢ ((𝐴:ℕ0⟶ℂ ∧
𝑚 ∈
ℕ0) → (𝐴‘𝑚) ∈ ℂ) | 
| 63 | 60, 61, 62 | syl2an 596 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑚 ∈ (0...(𝑖 − 1))) → (𝐴‘𝑚) ∈ ℂ) | 
| 64 | 59, 63 | fsumcl 15770 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴‘𝑚) ∈ ℂ) | 
| 65 |  | expcl 14121 | . . . . . . . . . 10
⊢ ((𝑋 ∈ ℂ ∧ 𝑖 ∈ ℕ0)
→ (𝑋↑𝑖) ∈
ℂ) | 
| 66 | 23, 65 | sylan 580 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑋↑𝑖) ∈ ℂ) | 
| 67 | 64, 66 | mulcld 11282 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
(Σ𝑚 ∈
(0...(𝑖 − 1))(𝐴‘𝑚) · (𝑋↑𝑖)) ∈ ℂ) | 
| 68 | 58, 67 | eqeltrd 2840 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑖) ∈ ℂ) | 
| 69 | 11 | peano2zd 12727 | . . . . . . . . 9
⊢ (𝜑 → (0 + 1) ∈
ℤ) | 
| 70 |  | nnuz 12922 | . . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) | 
| 71 |  | 1e0p1 12777 | . . . . . . . . . . . . 13
⊢ 1 = (0 +
1) | 
| 72 | 71 | fveq2i 6908 | . . . . . . . . . . . 12
⊢
(ℤ≥‘1) = (ℤ≥‘(0 +
1)) | 
| 73 | 70, 72 | eqtri 2764 | . . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘(0 + 1)) | 
| 74 | 73 | eleq2i 2832 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘(0 + 1))) | 
| 75 |  | nnm1nn0 12569 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) | 
| 76 | 75 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 − 1) ∈
ℕ0) | 
| 77 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑛 − 1) → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘(𝑛 − 1))) | 
| 78 |  | oveq2 7440 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑛 − 1) → (𝑋↑𝑘) = (𝑋↑(𝑛 − 1))) | 
| 79 | 77, 78 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑛 − 1) → ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)) = ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1)))) | 
| 80 | 79 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 − 1) → (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1))))) | 
| 81 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘)))) = (𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) | 
| 82 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢ (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1)))) ∈ V | 
| 83 | 80, 81, 82 | fvmpt 7015 | . . . . . . . . . . . 12
⊢ ((𝑛 − 1) ∈
ℕ0 → ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘(𝑛 − 1)) = (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1))))) | 
| 84 | 76, 83 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘(𝑛 − 1)) = (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1))))) | 
| 85 |  | ax-1cn 11214 | . . . . . . . . . . . 12
⊢ 1 ∈
ℂ | 
| 86 |  | nncn 12275 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) | 
| 87 | 86 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) | 
| 88 |  | nn0ex 12534 | . . . . . . . . . . . . . 14
⊢
ℕ0 ∈ V | 
| 89 | 88 | mptex 7244 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ V | 
| 90 | 89 | shftval 15114 | . . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ 𝑛
∈ ℂ) → (((𝑘
∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)‘𝑛) = ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘(𝑛 − 1))) | 
| 91 | 85, 87, 90 | sylancr 587 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)‘𝑛) = ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘(𝑛 − 1))) | 
| 92 |  | eqidd 2737 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → (𝐴‘𝑚) = (𝐴‘𝑚)) | 
| 93 | 76, 10 | eleqtrdi 2850 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 − 1) ∈
(ℤ≥‘0)) | 
| 94 | 19 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴:ℕ0⟶ℂ) | 
| 95 |  | elfznn0 13661 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (0...(𝑛 − 1)) → 𝑚 ∈ ℕ0) | 
| 96 | 94, 95, 62 | syl2an 596 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → (𝐴‘𝑚) ∈ ℂ) | 
| 97 | 92, 93, 96 | fsumser 15767 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) = (seq0( + , 𝐴)‘(𝑛 − 1))) | 
| 98 |  | expm1t 14132 | . . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ) → (𝑋↑𝑛) = ((𝑋↑(𝑛 − 1)) · 𝑋)) | 
| 99 | 23, 98 | sylan 580 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋↑𝑛) = ((𝑋↑(𝑛 − 1)) · 𝑋)) | 
| 100 | 23 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ ℂ) | 
| 101 |  | expcl 14121 | . . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ ℂ ∧ (𝑛 − 1) ∈
ℕ0) → (𝑋↑(𝑛 − 1)) ∈ ℂ) | 
| 102 | 23, 75, 101 | syl2an 596 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋↑(𝑛 − 1)) ∈ ℂ) | 
| 103 | 100, 102 | mulcomd 11283 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋 · (𝑋↑(𝑛 − 1))) = ((𝑋↑(𝑛 − 1)) · 𝑋)) | 
| 104 | 99, 103 | eqtr4d 2779 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋↑𝑛) = (𝑋 · (𝑋↑(𝑛 − 1)))) | 
| 105 | 97, 104 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛)) = ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋 · (𝑋↑(𝑛 − 1))))) | 
| 106 |  | nnnn0 12535 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) | 
| 107 | 106 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) | 
| 108 |  | oveq1 7439 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → (𝑘 − 1) = (𝑛 − 1)) | 
| 109 | 108 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (0...(𝑘 − 1)) = (0...(𝑛 − 1))) | 
| 110 | 109 | sumeq1d 15737 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) = Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚)) | 
| 111 | 110, 13 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛))) | 
| 112 |  | ovex 7465 | . . . . . . . . . . . . . 14
⊢
(Σ𝑚 ∈
(0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛)) ∈ V | 
| 113 | 111, 55, 112 | fvmpt 7015 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛))) | 
| 114 | 107, 113 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛))) | 
| 115 |  | ffvelcdm 7100 | . . . . . . . . . . . . . 14
⊢ ((seq0( +
, 𝐴):ℕ0⟶ℂ ∧
(𝑛 − 1) ∈
ℕ0) → (seq0( + , 𝐴)‘(𝑛 − 1)) ∈ ℂ) | 
| 116 | 33, 75, 115 | syl2an 596 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq0( + , 𝐴)‘(𝑛 − 1)) ∈ ℂ) | 
| 117 | 100, 116,
102 | mul12d 11471 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1)))) = ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋 · (𝑋↑(𝑛 − 1))))) | 
| 118 | 105, 114,
117 | 3eqtr4d 2786 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛) = (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1))))) | 
| 119 | 84, 91, 118 | 3eqtr4d 2786 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)‘𝑛) = ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛)) | 
| 120 | 74, 119 | sylan2br 595 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(0 +
1))) → (((𝑘 ∈
ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)‘𝑛) = ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛)) | 
| 121 | 69, 120 | seqfeq 14069 | . . . . . . . 8
⊢ (𝜑 → seq(0 + 1)( + , ((𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)) = seq(0 + 1)( + , (𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))) | 
| 122 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑖 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑖)) | 
| 123 | 122, 53 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) | 
| 124 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢ ((seq0( +
, 𝐴)‘𝑖) · (𝑋↑𝑖)) ∈ V | 
| 125 | 123, 29, 124 | fvmpt 7015 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) | 
| 126 | 125 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) | 
| 127 | 33 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (seq0( +
, 𝐴)‘𝑖) ∈
ℂ) | 
| 128 | 127, 66 | mulcld 11282 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((seq0( +
, 𝐴)‘𝑖) · (𝑋↑𝑖)) ∈ ℂ) | 
| 129 | 126, 128 | eqeltrd 2840 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) ∈ ℂ) | 
| 130 | 123 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))) | 
| 131 |  | ovex 7465 | . . . . . . . . . . . . 13
⊢ (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) ∈ V | 
| 132 | 130, 81, 131 | fvmpt 7015 | . . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑖) = (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))) | 
| 133 | 132 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑖) = (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))) | 
| 134 | 126 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑋 · ((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖)) = (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))) | 
| 135 | 133, 134 | eqtr4d 2779 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑖) = (𝑋 · ((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖))) | 
| 136 | 10, 11, 23, 45, 129, 135 | isermulc2 15695 | . . . . . . . . 9
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘))))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) | 
| 137 |  | 0z 12626 | . . . . . . . . . 10
⊢ 0 ∈
ℤ | 
| 138 |  | 1z 12649 | . . . . . . . . . 10
⊢ 1 ∈
ℤ | 
| 139 | 89 | isershft 15701 | . . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ↔ seq(0 + 1)( + , ((𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) | 
| 140 | 137, 138,
139 | mp2an 692 | . . . . . . . . 9
⊢ (seq0( +
, (𝑘 ∈
ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ↔ seq(0 + 1)( + , ((𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) | 
| 141 | 136, 140 | sylib 218 | . . . . . . . 8
⊢ (𝜑 → seq(0 + 1)( + , ((𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) | 
| 142 | 121, 141 | eqbrtrrd 5166 | . . . . . . 7
⊢ (𝜑 → seq(0 + 1)( + , (𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) | 
| 143 | 10, 49, 68, 142 | clim2ser2 15693 | . . . . . 6
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))) ⇝ ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + (seq0( + , (𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘0))) | 
| 144 |  | seq1 14056 | . . . . . . . . . . 11
⊢ (0 ∈
ℤ → (seq0( + , (𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘0)) | 
| 145 | 137, 144 | ax-mp 5 | . . . . . . . . . 10
⊢ (seq0( +
, (𝑘 ∈
ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘0) | 
| 146 |  | oveq1 7439 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1)) | 
| 147 | 146 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = 0 → (0...(𝑘 − 1)) = (0...(0 −
1))) | 
| 148 |  | risefall0lem 16063 | . . . . . . . . . . . . . . . 16
⊢ (0...(0
− 1)) = ∅ | 
| 149 | 147, 148 | eqtrdi 2792 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 0 → (0...(𝑘 − 1)) =
∅) | 
| 150 | 149 | sumeq1d 15737 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 0 → Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) = Σ𝑚 ∈ ∅ (𝐴‘𝑚)) | 
| 151 |  | sum0 15758 | . . . . . . . . . . . . . 14
⊢
Σ𝑚 ∈
∅ (𝐴‘𝑚) = 0 | 
| 152 | 150, 151 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ (𝑘 = 0 → Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) = 0) | 
| 153 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (𝑋↑𝑘) = (𝑋↑0)) | 
| 154 | 152, 153 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (𝑘 = 0 → (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)) = (0 · (𝑋↑0))) | 
| 155 |  | ovex 7465 | . . . . . . . . . . . 12
⊢ (0
· (𝑋↑0)) ∈
V | 
| 156 | 154, 55, 155 | fvmpt 7015 | . . . . . . . . . . 11
⊢ (0 ∈
ℕ0 → ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘0) = (0 · (𝑋↑0))) | 
| 157 | 48, 156 | ax-mp 5 | . . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘0) = (0 · (𝑋↑0)) | 
| 158 | 145, 157 | eqtri 2764 | . . . . . . . . 9
⊢ (seq0( +
, (𝑘 ∈
ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘0) = (0 · (𝑋↑0)) | 
| 159 |  | expcl 14121 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ ℂ ∧ 0 ∈
ℕ0) → (𝑋↑0) ∈ ℂ) | 
| 160 | 23, 48, 159 | sylancl 586 | . . . . . . . . . 10
⊢ (𝜑 → (𝑋↑0) ∈ ℂ) | 
| 161 | 160 | mul02d 11460 | . . . . . . . . 9
⊢ (𝜑 → (0 · (𝑋↑0)) = 0) | 
| 162 | 158, 161 | eqtrid 2788 | . . . . . . . 8
⊢ (𝜑 → (seq0( + , (𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘0) = 0) | 
| 163 | 162 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + (seq0( + , (𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘0)) = ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + 0)) | 
| 164 | 10, 11, 32, 35, 44 | isumcl 15798 | . . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) | 
| 165 | 23, 164 | mulcld 11282 | . . . . . . . 8
⊢ (𝜑 → (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℂ) | 
| 166 | 165 | addridd 11462 | . . . . . . 7
⊢ (𝜑 → ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + 0) = (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) | 
| 167 | 163, 166 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + (seq0( + , (𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘0)) = (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) | 
| 168 | 143, 167 | breqtrd 5168 | . . . . 5
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) | 
| 169 | 10, 11, 129 | serf 14072 | . . . . . 6
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))):ℕ0⟶ℂ) | 
| 170 | 169 | ffvelcdmda 7103 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (seq0( +
, (𝑘 ∈
ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑖) ∈ ℂ) | 
| 171 | 10, 11, 68 | serf 14072 | . . . . . 6
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))):ℕ0⟶ℂ) | 
| 172 | 171 | ffvelcdmda 7103 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (seq0( +
, (𝑘 ∈
ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘𝑖) ∈ ℂ) | 
| 173 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
ℕ0) | 
| 174 | 173, 10 | eleqtrdi 2850 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
(ℤ≥‘0)) | 
| 175 |  | simpl 482 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝜑) | 
| 176 |  | elfznn0 13661 | . . . . . . 7
⊢ (𝑛 ∈ (0...𝑖) → 𝑛 ∈ ℕ0) | 
| 177 | 32, 35 | eqeltrd 2840 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) ∈ ℂ) | 
| 178 | 175, 176,
177 | syl2an 596 | . . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑛 ∈ (0...𝑖)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) ∈ ℂ) | 
| 179 | 113 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛))) | 
| 180 |  | fzfid 14015 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(0...(𝑛 − 1)) ∈
Fin) | 
| 181 | 19 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝐴:ℕ0⟶ℂ) | 
| 182 | 181, 95, 62 | syl2an 596 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → (𝐴‘𝑚) ∈ ℂ) | 
| 183 | 180, 182 | fsumcl 15770 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) ∈ ℂ) | 
| 184 | 183, 25 | mulcld 11282 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(Σ𝑚 ∈
(0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛)) ∈ ℂ) | 
| 185 | 179, 184 | eqeltrd 2840 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛) ∈ ℂ) | 
| 186 | 175, 176,
185 | syl2an 596 | . . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑛 ∈ (0...𝑖)) → ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛) ∈ ℂ) | 
| 187 |  | eqidd 2737 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑚 ∈ (0...𝑛)) → (𝐴‘𝑚) = (𝐴‘𝑚)) | 
| 188 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) | 
| 189 | 188, 10 | eleqtrdi 2850 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
(ℤ≥‘0)) | 
| 190 |  | elfznn0 13661 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (0...𝑛) → 𝑚 ∈ ℕ0) | 
| 191 | 181, 190,
62 | syl2an 596 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑚 ∈ (0...𝑛)) → (𝐴‘𝑚) ∈ ℂ) | 
| 192 | 187, 189,
191 | fsumser 15767 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
Σ𝑚 ∈ (0...𝑛)(𝐴‘𝑚) = (seq0( + , 𝐴)‘𝑛)) | 
| 193 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝐴‘𝑚) = (𝐴‘𝑛)) | 
| 194 | 189, 191,
193 | fsumm1 15788 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
Σ𝑚 ∈ (0...𝑛)(𝐴‘𝑚) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) + (𝐴‘𝑛))) | 
| 195 | 192, 194 | eqtr3d 2778 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (seq0( +
, 𝐴)‘𝑛) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) + (𝐴‘𝑛))) | 
| 196 | 195 | oveq1d 7447 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((seq0( +
, 𝐴)‘𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚)) = ((Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) + (𝐴‘𝑛)) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚))) | 
| 197 | 183, 20 | pncan2d 11623 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((Σ𝑚 ∈
(0...(𝑛 − 1))(𝐴‘𝑚) + (𝐴‘𝑛)) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚)) = (𝐴‘𝑛)) | 
| 198 | 196, 197 | eqtr2d 2777 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐴‘𝑛) = ((seq0( + , 𝐴)‘𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚))) | 
| 199 | 198 | oveq1d 7447 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝐴‘𝑛) · (𝑋↑𝑛)) = (((seq0( + , 𝐴)‘𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚)) · (𝑋↑𝑛))) | 
| 200 | 34, 183, 25 | subdird 11721 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((seq0(
+ , 𝐴)‘𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚)) · (𝑋↑𝑛)) = (((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) − (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛)))) | 
| 201 | 199, 200 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝐴‘𝑛) · (𝑋↑𝑛)) = (((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) − (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛)))) | 
| 202 | 32, 179 | oveq12d 7450 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) − ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛)) = (((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) − (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛)))) | 
| 203 | 201, 18, 202 | 3eqtr4d 2786 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))‘𝑛) = (((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) − ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛))) | 
| 204 | 175, 176,
203 | syl2an 596 | . . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑛 ∈ (0...𝑖)) → ((𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))‘𝑛) = (((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) − ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛))) | 
| 205 | 174, 178,
186, 204 | sersub 14087 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (seq0( +
, (𝑘 ∈
ℕ0 ↦ ((𝐴‘𝑘) · (𝑋↑𝑘))))‘𝑖) = ((seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑖) − (seq0( + , (𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘𝑖))) | 
| 206 | 10, 11, 45, 47, 168, 170, 172, 205 | climsub 15671 | . . . 4
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))) ⇝ (Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) | 
| 207 |  | 1cnd 11257 | . . . . . 6
⊢ (𝜑 → 1 ∈
ℂ) | 
| 208 | 207, 23, 164 | subdird 11721 | . . . . 5
⊢ (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ ℕ0
((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = ((1 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) | 
| 209 | 164 | mullidd 11280 | . . . . . 6
⊢ (𝜑 → (1 · Σ𝑛 ∈ ℕ0
((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) | 
| 210 | 209 | oveq1d 7447 | . . . . 5
⊢ (𝜑 → ((1 · Σ𝑛 ∈ ℕ0
((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = (Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) | 
| 211 | 208, 210 | eqtrd 2776 | . . . 4
⊢ (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ ℕ0
((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = (Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) | 
| 212 | 206, 211 | breqtrrd 5170 | . . 3
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))) ⇝ ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) | 
| 213 | 10, 11, 18, 26, 212 | isumclim 15794 | . 2
⊢ (𝜑 → Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑋↑𝑛)) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) | 
| 214 | 9, 213 | eqtrd 2776 | 1
⊢ (𝜑 → (𝐹‘𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |