| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nn0uz 12920 | . 2
⊢
ℕ0 = (ℤ≥‘0) | 
| 2 |  | 1nn0 12542 | . . 3
⊢ 1 ∈
ℕ0 | 
| 3 | 2 | a1i 11 | . 2
⊢ (𝜑 → 1 ∈
ℕ0) | 
| 4 |  | ax-1cn 11213 | . . . . 5
⊢ 1 ∈
ℂ | 
| 5 |  | nn0cn 12536 | . . . . . 6
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) | 
| 6 | 5 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℂ) | 
| 7 |  | nn0ex 12532 | . . . . . . 7
⊢
ℕ0 ∈ V | 
| 8 | 7 | mptex 7243 | . . . . . 6
⊢ (𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))) ∈ V | 
| 9 | 8 | shftval4 15116 | . . . . 5
⊢ ((1
∈ ℂ ∧ 𝑘
∈ ℂ) → (((𝑖
∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘))) | 
| 10 | 4, 6, 9 | sylancr 587 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘))) | 
| 11 |  | addcom 11447 | . . . . . 6
⊢ ((1
∈ ℂ ∧ 𝑘
∈ ℂ) → (1 + 𝑘) = (𝑘 + 1)) | 
| 12 | 4, 6, 11 | sylancr 587 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 +
𝑘) = (𝑘 + 1)) | 
| 13 | 12 | fveq2d 6910 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) = ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1))) | 
| 14 |  | peano2nn0 12566 | . . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) | 
| 15 | 14 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈
ℕ0) | 
| 16 |  | id 22 | . . . . . . . 8
⊢ (𝑖 = (𝑘 + 1) → 𝑖 = (𝑘 + 1)) | 
| 17 |  | 2fveq3 6911 | . . . . . . . 8
⊢ (𝑖 = (𝑘 + 1) → (abs‘((𝐺‘𝑋)‘𝑖)) = (abs‘((𝐺‘𝑋)‘(𝑘 + 1)))) | 
| 18 | 16, 17 | oveq12d 7449 | . . . . . . 7
⊢ (𝑖 = (𝑘 + 1) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) = ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1))))) | 
| 19 |  | eqid 2737 | . . . . . . 7
⊢ (𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))) = (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) | 
| 20 |  | ovex 7464 | . . . . . . 7
⊢ ((𝑘 + 1) ·
(abs‘((𝐺‘𝑋)‘(𝑘 + 1)))) ∈ V | 
| 21 | 18, 19, 20 | fvmpt 7016 | . . . . . 6
⊢ ((𝑘 + 1) ∈ ℕ0
→ ((𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)) = ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1))))) | 
| 22 | 15, 21 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)) = ((𝑘 + 1) · (abs‘((𝐺‘𝑋)‘(𝑘 + 1))))) | 
| 23 |  | dvradcnv.x | . . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 24 |  | dvradcnv.g | . . . . . . . . 9
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) | 
| 25 | 24 | pserval2 26454 | . . . . . . . 8
⊢ ((𝑋 ∈ ℂ ∧ (𝑘 + 1) ∈
ℕ0) → ((𝐺‘𝑋)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) | 
| 26 | 23, 14, 25 | syl2an 596 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑋)‘(𝑘 + 1)) = ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) | 
| 27 | 26 | fveq2d 6910 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘((𝐺‘𝑋)‘(𝑘 + 1))) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) | 
| 28 | 27 | oveq2d 7447 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) ·
(abs‘((𝐺‘𝑋)‘(𝑘 + 1)))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) | 
| 29 | 22, 28 | eqtrd 2777 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖))))‘(𝑘 + 1)) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) | 
| 30 | 10, 13, 29 | 3eqtrd 2781 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) | 
| 31 | 15 | nn0red 12588 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈
ℝ) | 
| 32 |  | dvradcnv.a | . . . . . . 7
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) | 
| 33 |  | ffvelcdm 7101 | . . . . . . 7
⊢ ((𝐴:ℕ0⟶ℂ ∧
(𝑘 + 1) ∈
ℕ0) → (𝐴‘(𝑘 + 1)) ∈ ℂ) | 
| 34 | 32, 14, 33 | syl2an 596 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘(𝑘 + 1)) ∈ ℂ) | 
| 35 |  | expcl 14120 | . . . . . . 7
⊢ ((𝑋 ∈ ℂ ∧ (𝑘 + 1) ∈
ℕ0) → (𝑋↑(𝑘 + 1)) ∈ ℂ) | 
| 36 | 23, 14, 35 | syl2an 596 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑋↑(𝑘 + 1)) ∈ ℂ) | 
| 37 | 34, 36 | mulcld 11281 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) ∈ ℂ) | 
| 38 | 37 | abscld 15475 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℝ) | 
| 39 | 31, 38 | remulcld 11291 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) ·
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) ∈ ℝ) | 
| 40 | 30, 39 | eqeltrd 2841 | . 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) ∈ ℝ) | 
| 41 |  | oveq1 7438 | . . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1)) | 
| 42 | 41 | fveq2d 6910 | . . . . . . 7
⊢ (𝑛 = 𝑘 → (𝐴‘(𝑛 + 1)) = (𝐴‘(𝑘 + 1))) | 
| 43 | 41, 42 | oveq12d 7449 | . . . . . 6
⊢ (𝑛 = 𝑘 → ((𝑛 + 1) · (𝐴‘(𝑛 + 1))) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1)))) | 
| 44 |  | oveq2 7439 | . . . . . 6
⊢ (𝑛 = 𝑘 → (𝑋↑𝑛) = (𝑋↑𝑘)) | 
| 45 | 43, 44 | oveq12d 7449 | . . . . 5
⊢ (𝑛 = 𝑘 → (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) | 
| 46 |  | dvradcnv.h | . . . . 5
⊢ 𝐻 = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑋↑𝑛))) | 
| 47 |  | ovex 7464 | . . . . 5
⊢ (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) ∈ V | 
| 48 | 45, 46, 47 | fvmpt 7016 | . . . 4
⊢ (𝑘 ∈ ℕ0
→ (𝐻‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) | 
| 49 | 48 | adantl 481 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) | 
| 50 | 15 | nn0cnd 12589 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈
ℂ) | 
| 51 | 50, 34 | mulcld 11281 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) ∈ ℂ) | 
| 52 |  | expcl 14120 | . . . . 5
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑋↑𝑘) ∈
ℂ) | 
| 53 | 23, 52 | sylan 580 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑋↑𝑘) ∈ ℂ) | 
| 54 | 51, 53 | mulcld 11281 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) ∈ ℂ) | 
| 55 | 49, 54 | eqeltrd 2841 | . 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) ∈ ℂ) | 
| 56 |  | dvradcnv.r | . . . . . . . 8
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) | 
| 57 |  | dvradcnv.l | . . . . . . . 8
⊢ (𝜑 → (abs‘𝑋) < 𝑅) | 
| 58 |  | id 22 | . . . . . . . . . 10
⊢ (𝑖 = 𝑘 → 𝑖 = 𝑘) | 
| 59 |  | 2fveq3 6911 | . . . . . . . . . 10
⊢ (𝑖 = 𝑘 → (abs‘((𝐺‘𝑋)‘𝑖)) = (abs‘((𝐺‘𝑋)‘𝑘))) | 
| 60 | 58, 59 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑖 = 𝑘 → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) | 
| 61 | 60 | cbvmptv 5255 | . . . . . . . 8
⊢ (𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))) = (𝑘 ∈ ℕ0 ↦ (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) | 
| 62 | 24, 32, 56, 23, 57, 61 | radcnvlt1 26461 | . . . . . . 7
⊢ (𝜑 → (seq0( + , (𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ ∧ seq0( + , (abs
∘ (𝐺‘𝑋))) ∈ dom ⇝
)) | 
| 63 | 62 | simpld 494 | . . . . . 6
⊢ (𝜑 → seq0( + , (𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ ) | 
| 64 |  | climdm 15590 | . . . . . 6
⊢ (seq0( +
, (𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ∈ dom ⇝ ↔ seq0( + ,
(𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + ,
(𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))))) | 
| 65 | 63, 64 | sylib 218 | . . . . 5
⊢ (𝜑 → seq0( + , (𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + ,
(𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))))) | 
| 66 |  | 0z 12624 | . . . . . 6
⊢ 0 ∈
ℤ | 
| 67 |  | neg1z 12653 | . . . . . 6
⊢ -1 ∈
ℤ | 
| 68 | 8 | isershft 15700 | . . . . . 6
⊢ ((0
∈ ℤ ∧ -1 ∈ ℤ) → (seq0( + , (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + ,
(𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ↔ seq(0 + -1)( + , ((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝
‘seq0( + , (𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))))) | 
| 69 | 66, 67, 68 | mp2an 692 | . . . . 5
⊢ (seq0( +
, (𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))) ⇝ ( ⇝ ‘seq0( + ,
(𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ↔ seq(0 + -1)( + , ((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝
‘seq0( + , (𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))))) | 
| 70 | 65, 69 | sylib 218 | . . . 4
⊢ (𝜑 → seq(0 + -1)( + , ((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝
‘seq0( + , (𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))))) | 
| 71 |  | seqex 14044 | . . . . 5
⊢ seq(0 +
-1)( + , ((𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ V | 
| 72 |  | fvex 6919 | . . . . 5
⊢ ( ⇝
‘seq0( + , (𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) ∈ V | 
| 73 | 71, 72 | breldm 5919 | . . . 4
⊢ (seq(0 +
-1)( + , ((𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ⇝ ( ⇝
‘seq0( + , (𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))))) → seq(0 + -1)( + , ((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝
) | 
| 74 | 70, 73 | syl 17 | . . 3
⊢ (𝜑 → seq(0 + -1)( + , ((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝
) | 
| 75 |  | eqid 2737 | . . . 4
⊢
(ℤ≥‘(0 + -1)) =
(ℤ≥‘(0 + -1)) | 
| 76 |  | neg1cn 12380 | . . . . . . . 8
⊢ -1 ∈
ℂ | 
| 77 | 76 | addlidi 11449 | . . . . . . 7
⊢ (0 + -1)
= -1 | 
| 78 |  | 0le1 11786 | . . . . . . . 8
⊢ 0 ≤
1 | 
| 79 |  | 1re 11261 | . . . . . . . . 9
⊢ 1 ∈
ℝ | 
| 80 |  | le0neg2 11772 | . . . . . . . . 9
⊢ (1 ∈
ℝ → (0 ≤ 1 ↔ -1 ≤ 0)) | 
| 81 | 79, 80 | ax-mp 5 | . . . . . . . 8
⊢ (0 ≤ 1
↔ -1 ≤ 0) | 
| 82 | 78, 81 | mpbi 230 | . . . . . . 7
⊢ -1 ≤
0 | 
| 83 | 77, 82 | eqbrtri 5164 | . . . . . 6
⊢ (0 + -1)
≤ 0 | 
| 84 | 77, 67 | eqeltri 2837 | . . . . . . 7
⊢ (0 + -1)
∈ ℤ | 
| 85 | 84 | eluz1i 12886 | . . . . . 6
⊢ (0 ∈
(ℤ≥‘(0 + -1)) ↔ (0 ∈ ℤ ∧ (0 + -1)
≤ 0)) | 
| 86 | 66, 83, 85 | mpbir2an 711 | . . . . 5
⊢ 0 ∈
(ℤ≥‘(0 + -1)) | 
| 87 | 86 | a1i 11 | . . . 4
⊢ (𝜑 → 0 ∈
(ℤ≥‘(0 + -1))) | 
| 88 |  | eluzelcn 12890 | . . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘(0 + -1)) → 𝑘 ∈ ℂ) | 
| 89 | 88 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 +
-1))) → 𝑘 ∈
ℂ) | 
| 90 | 4, 89, 9 | sylancr 587 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 +
-1))) → (((𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘))) | 
| 91 |  | nn0re 12535 | . . . . . . . . . 10
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) | 
| 92 | 91 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
ℝ) | 
| 93 | 24, 32, 23 | psergf 26455 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐺‘𝑋):ℕ0⟶ℂ) | 
| 94 | 93 | ffvelcdmda 7104 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝐺‘𝑋)‘𝑖) ∈ ℂ) | 
| 95 | 94 | abscld 15475 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
(abs‘((𝐺‘𝑋)‘𝑖)) ∈ ℝ) | 
| 96 | 92, 95 | remulcld 11291 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) ∈ ℝ) | 
| 97 | 96 | recnd 11289 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))) ∈ ℂ) | 
| 98 | 97 | fmpttd 7135 | . . . . . 6
⊢ (𝜑 → (𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))):ℕ0⟶ℂ) | 
| 99 | 4, 88, 11 | sylancr 587 | . . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘(0 + -1)) → (1 + 𝑘) = (𝑘 + 1)) | 
| 100 |  | eluzp1p1 12906 | . . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘(0 + -1)) → (𝑘 + 1) ∈
(ℤ≥‘((0 + -1) + 1))) | 
| 101 | 77 | oveq1i 7441 | . . . . . . . . . . 11
⊢ ((0 + -1)
+ 1) = (-1 + 1) | 
| 102 |  | 1pneg1e0 12385 | . . . . . . . . . . . 12
⊢ (1 + -1)
= 0 | 
| 103 | 4, 76, 102 | addcomli 11453 | . . . . . . . . . . 11
⊢ (-1 + 1)
= 0 | 
| 104 | 101, 103 | eqtri 2765 | . . . . . . . . . 10
⊢ ((0 + -1)
+ 1) = 0 | 
| 105 | 104 | fveq2i 6909 | . . . . . . . . 9
⊢
(ℤ≥‘((0 + -1) + 1)) =
(ℤ≥‘0) | 
| 106 | 1, 105 | eqtr4i 2768 | . . . . . . . 8
⊢
ℕ0 = (ℤ≥‘((0 + -1) +
1)) | 
| 107 | 100, 106 | eleqtrrdi 2852 | . . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘(0 + -1)) → (𝑘 + 1) ∈
ℕ0) | 
| 108 | 99, 107 | eqeltrd 2841 | . . . . . 6
⊢ (𝑘 ∈
(ℤ≥‘(0 + -1)) → (1 + 𝑘) ∈
ℕ0) | 
| 109 |  | ffvelcdm 7101 | . . . . . 6
⊢ (((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))):ℕ0⟶ℂ ∧
(1 + 𝑘) ∈
ℕ0) → ((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) ∈ ℂ) | 
| 110 | 98, 108, 109 | syl2an 596 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 +
-1))) → ((𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖))))‘(1 + 𝑘)) ∈ ℂ) | 
| 111 | 90, 110 | eqeltrd 2841 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(0 +
-1))) → (((𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘) ∈ ℂ) | 
| 112 | 75, 87, 111 | iserex 15693 | . . 3
⊢ (𝜑 → (seq(0 + -1)( + , ((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝ ↔
seq0( + , ((𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝
)) | 
| 113 | 74, 112 | mpbid 232 | . 2
⊢ (𝜑 → seq0( + , ((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)) ∈ dom ⇝
) | 
| 114 |  | 1red 11262 | . . 3
⊢ ((𝜑 ∧ 𝑋 = 0) → 1 ∈
ℝ) | 
| 115 |  | neqne 2948 | . . . . 5
⊢ (¬
𝑋 = 0 → 𝑋 ≠ 0) | 
| 116 |  | absrpcl 15327 | . . . . 5
⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈
ℝ+) | 
| 117 | 23, 115, 116 | syl2an 596 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝑋 = 0) → (abs‘𝑋) ∈
ℝ+) | 
| 118 | 117 | rprecred 13088 | . . 3
⊢ ((𝜑 ∧ ¬ 𝑋 = 0) → (1 / (abs‘𝑋)) ∈
ℝ) | 
| 119 | 114, 118 | ifclda 4561 | . 2
⊢ (𝜑 → if(𝑋 = 0, 1, (1 / (abs‘𝑋))) ∈ ℝ) | 
| 120 |  | oveq1 7438 | . . . . 5
⊢ (1 =
if(𝑋 = 0, 1, (1 /
(abs‘𝑋))) → (1
· ((𝑘 + 1) ·
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))) | 
| 121 | 120 | breq2d 5155 | . . . 4
⊢ (1 =
if(𝑋 = 0, 1, (1 /
(abs‘𝑋))) →
((abs‘(((𝑘 + 1)
· (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) ↔ (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))) | 
| 122 |  | oveq1 7438 | . . . . 5
⊢ ((1 /
(abs‘𝑋)) = if(𝑋 = 0, 1, (1 / (abs‘𝑋))) → ((1 /
(abs‘𝑋)) ·
((𝑘 + 1) ·
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))) | 
| 123 | 122 | breq2d 5155 | . . . 4
⊢ ((1 /
(abs‘𝑋)) = if(𝑋 = 0, 1, (1 / (abs‘𝑋))) → ((abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) ↔ (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))))) | 
| 124 |  | elnnuz 12922 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) | 
| 125 |  | nnnn0 12533 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) | 
| 126 | 124, 125 | sylbir 235 | . . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘1) → 𝑘 ∈ ℕ0) | 
| 127 | 15 | nn0ge0d 12590 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤
(𝑘 + 1)) | 
| 128 | 37 | absge0d 15483 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) | 
| 129 | 31, 38, 127, 128 | mulge0d 11840 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤
((𝑘 + 1) ·
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) | 
| 130 | 126, 129 | sylan2 593 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ 0 ≤ ((𝑘 + 1)
· (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) | 
| 131 | 130 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
∧ 𝑋 = 0) → 0 ≤
((𝑘 + 1) ·
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) | 
| 132 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑋 = 0 → (𝑋↑𝑘) = (0↑𝑘)) | 
| 133 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ 𝑘 ∈
(ℤ≥‘1)) | 
| 134 | 133, 124 | sylibr 234 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ 𝑘 ∈
ℕ) | 
| 135 | 134 | 0expd 14179 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (0↑𝑘) =
0) | 
| 136 | 132, 135 | sylan9eqr 2799 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
∧ 𝑋 = 0) → (𝑋↑𝑘) = 0) | 
| 137 | 136 | oveq2d 7447 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
∧ 𝑋 = 0) →
(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0)) | 
| 138 | 51 | mul01d 11460 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0) = 0) | 
| 139 | 126, 138 | sylan2 593 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (((𝑘 + 1) ·
(𝐴‘(𝑘 + 1))) · 0) =
0) | 
| 140 | 139 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
∧ 𝑋 = 0) →
(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · 0) = 0) | 
| 141 | 137, 140 | eqtrd 2777 | . . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
∧ 𝑋 = 0) →
(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = 0) | 
| 142 | 141 | abs00bd 15330 | . . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
∧ 𝑋 = 0) →
(abs‘(((𝑘 + 1)
· (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = 0) | 
| 143 | 39 | recnd 11289 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑘 + 1) ·
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) ∈ ℂ) | 
| 144 | 143 | mullidd 11279 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1
· ((𝑘 + 1) ·
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) | 
| 145 | 126, 144 | sylan2 593 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (1 · ((𝑘 + 1)
· (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) | 
| 146 | 145 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
∧ 𝑋 = 0) → (1
· ((𝑘 + 1) ·
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) | 
| 147 | 131, 142,
146 | 3brtr4d 5175 | . . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
∧ 𝑋 = 0) →
(abs‘(((𝑘 + 1)
· (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (1 · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))) | 
| 148 |  | df-ne 2941 | . . . . 5
⊢ (𝑋 ≠ 0 ↔ ¬ 𝑋 = 0) | 
| 149 | 54 | abscld 15475 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘(((𝑘 + 1)
· (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ∈ ℝ) | 
| 150 | 50, 34, 53 | mulassd 11284 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) | 
| 151 | 150 | fveq2d 6910 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘(((𝑘 + 1)
· (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = (abs‘((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))) | 
| 152 | 34, 53 | mulcld 11281 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)) ∈ ℂ) | 
| 153 | 50, 152 | absmuld 15493 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘((𝑘 + 1)
· ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) = ((abs‘(𝑘 + 1)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))) | 
| 154 | 31, 127 | absidd 15461 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘(𝑘 + 1)) =
(𝑘 + 1)) | 
| 155 | 154 | oveq1d 7446 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((abs‘(𝑘 + 1))
· (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))) | 
| 156 | 151, 153,
155 | 3eqtrd 2781 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘(((𝑘 + 1)
· (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))) | 
| 157 | 149, 156 | eqled 11364 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘(((𝑘 + 1)
· (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))) | 
| 158 | 157 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) →
(abs‘(((𝑘 + 1)
· (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))) | 
| 159 | 23 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑋 ∈
ℂ) | 
| 160 | 116 | rpreccld 13087 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ ℂ ∧ 𝑋 ≠ 0) → (1 /
(abs‘𝑋)) ∈
ℝ+) | 
| 161 | 159, 160 | sylan 580 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (1 /
(abs‘𝑋)) ∈
ℝ+) | 
| 162 | 161 | rpcnd 13079 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (1 /
(abs‘𝑋)) ∈
ℂ) | 
| 163 | 50 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑘 + 1) ∈
ℂ) | 
| 164 | 38 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) →
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℝ) | 
| 165 | 164 | recnd 11289 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) →
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) ∈ ℂ) | 
| 166 | 162, 163,
165 | mul12d 11470 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((1 /
(abs‘𝑋)) ·
((𝑘 + 1) ·
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))) | 
| 167 | 37 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) ∈ ℂ) | 
| 168 | 23 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → 𝑋 ∈
ℂ) | 
| 169 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → 𝑋 ≠ 0) | 
| 170 | 167, 168,
169 | absdivd 15494 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) →
(abs‘(((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋)) = ((abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) / (abs‘𝑋))) | 
| 171 | 34 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝐴‘(𝑘 + 1)) ∈ ℂ) | 
| 172 | 36 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑋↑(𝑘 + 1)) ∈ ℂ) | 
| 173 | 171, 172,
168, 169 | divassd 12078 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋) = ((𝐴‘(𝑘 + 1)) · ((𝑋↑(𝑘 + 1)) / 𝑋))) | 
| 174 | 6 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → 𝑘 ∈
ℂ) | 
| 175 |  | pncan 11514 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) | 
| 176 | 174, 4, 175 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((𝑘 + 1) − 1) = 𝑘) | 
| 177 | 176 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑋↑((𝑘 + 1) − 1)) = (𝑋↑𝑘)) | 
| 178 | 15 | nn0zd 12639 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 + 1) ∈
ℤ) | 
| 179 | 178 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑘 + 1) ∈
ℤ) | 
| 180 | 168, 169,
179 | expm1d 14196 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑋↑((𝑘 + 1) − 1)) = ((𝑋↑(𝑘 + 1)) / 𝑋)) | 
| 181 | 177, 180 | eqtr3d 2779 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (𝑋↑𝑘) = ((𝑋↑(𝑘 + 1)) / 𝑋)) | 
| 182 | 181 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)) = ((𝐴‘(𝑘 + 1)) · ((𝑋↑(𝑘 + 1)) / 𝑋))) | 
| 183 | 173, 182 | eqtr4d 2780 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋) = ((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))) | 
| 184 | 183 | fveq2d 6910 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) →
(abs‘(((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))) / 𝑋)) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) | 
| 185 | 23 | abscld 15475 | . . . . . . . . . . . . 13
⊢ (𝜑 → (abs‘𝑋) ∈
ℝ) | 
| 186 | 185 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈
ℝ) | 
| 187 | 186 | recnd 11289 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈
ℂ) | 
| 188 | 159, 116 | sylan 580 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ∈
ℝ+) | 
| 189 | 188 | rpne0d 13082 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → (abs‘𝑋) ≠ 0) | 
| 190 | 165, 187,
189 | divrec2d 12047 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) →
((abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))) / (abs‘𝑋)) = ((1 / (abs‘𝑋)) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) | 
| 191 | 170, 184,
190 | 3eqtr3rd 2786 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((1 /
(abs‘𝑋)) ·
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))) = (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘)))) | 
| 192 | 191 | oveq2d 7447 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((𝑘 + 1) · ((1 /
(abs‘𝑋)) ·
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))) | 
| 193 | 166, 192 | eqtrd 2777 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) → ((1 /
(abs‘𝑋)) ·
((𝑘 + 1) ·
(abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1)))))) = ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑𝑘))))) | 
| 194 | 158, 193 | breqtrrd 5171 | . . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑋 ≠ 0) →
(abs‘(((𝑘 + 1)
· (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))) | 
| 195 | 126, 194 | sylanl2 681 | . . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
∧ 𝑋 ≠ 0) →
(abs‘(((𝑘 + 1)
· (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))) | 
| 196 | 148, 195 | sylan2br 595 | . . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
∧ ¬ 𝑋 = 0) →
(abs‘(((𝑘 + 1)
· (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ ((1 / (abs‘𝑋)) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))) | 
| 197 | 121, 123,
147, 196 | ifbothda 4564 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (abs‘(((𝑘 + 1)
· (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘))) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))) | 
| 198 | 49 | fveq2d 6910 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘(𝐻‘𝑘)) = (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))) | 
| 199 | 126, 198 | sylan2 593 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (abs‘(𝐻‘𝑘)) = (abs‘(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑋↑𝑘)))) | 
| 200 | 30 | oveq2d 7447 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ0
↦ (𝑖 ·
(abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))) | 
| 201 | 126, 200 | sylan2 593 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (if(𝑋 = 0, 1, (1 /
(abs‘𝑋))) ·
(((𝑖 ∈
ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘)) = (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · ((𝑘 + 1) · (abs‘((𝐴‘(𝑘 + 1)) · (𝑋↑(𝑘 + 1))))))) | 
| 202 | 197, 199,
201 | 3brtr4d 5175 | . 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (abs‘(𝐻‘𝑘)) ≤ (if(𝑋 = 0, 1, (1 / (abs‘𝑋))) · (((𝑖 ∈ ℕ0 ↦ (𝑖 · (abs‘((𝐺‘𝑋)‘𝑖)))) shift -1)‘𝑘))) | 
| 203 | 1, 3, 40, 55, 113, 119, 202 | cvgcmpce 15854 | 1
⊢ (𝜑 → seq0( + , 𝐻) ∈ dom ⇝
) |