| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | abelth.1 | . . . . . . 7
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) | 
| 2 |  | abelth.2 | . . . . . . 7
⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝
) | 
| 3 |  | abelth.3 | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 4 |  | abelth.4 | . . . . . . 7
⊢ (𝜑 → 0 ≤ 𝑀) | 
| 5 |  | abelth.5 | . . . . . . 7
⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} | 
| 6 | 1, 2, 3, 4, 5 | abelthlem2 26476 | . . . . . 6
⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1))) | 
| 7 | 6 | simprd 495 | . . . . 5
⊢ (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1)) | 
| 8 |  | ssundif 4488 | . . . . 5
⊢ (𝑆 ⊆ ({1} ∪
(0(ball‘(abs ∘ − ))1)) ↔ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1)) | 
| 9 | 7, 8 | sylibr 234 | . . . 4
⊢ (𝜑 → 𝑆 ⊆ ({1} ∪ (0(ball‘(abs
∘ − ))1))) | 
| 10 | 9 | sselda 3983 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → 𝑋 ∈ ({1} ∪ (0(ball‘(abs
∘ − ))1))) | 
| 11 |  | elun 4153 | . . 3
⊢ (𝑋 ∈ ({1} ∪
(0(ball‘(abs ∘ − ))1)) ↔ (𝑋 ∈ {1} ∨ 𝑋 ∈ (0(ball‘(abs ∘ −
))1))) | 
| 12 | 10, 11 | sylib 218 | . 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → (𝑋 ∈ {1} ∨ 𝑋 ∈ (0(ball‘(abs ∘ −
))1))) | 
| 13 | 1 | feqmptd 6977 | . . . . . . 7
⊢ (𝜑 → 𝐴 = (𝑛 ∈ ℕ0 ↦ (𝐴‘𝑛))) | 
| 14 | 1 | ffvelcdmda 7104 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐴‘𝑛) ∈ ℂ) | 
| 15 | 14 | mulridd 11278 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝐴‘𝑛) · 1) = (𝐴‘𝑛)) | 
| 16 | 15 | mpteq2dva 5242 | . . . . . . 7
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · 1)) = (𝑛 ∈ ℕ0 ↦ (𝐴‘𝑛))) | 
| 17 | 13, 16 | eqtr4d 2780 | . . . . . 6
⊢ (𝜑 → 𝐴 = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · 1))) | 
| 18 |  | elsni 4643 | . . . . . . . . . . 11
⊢ (𝑋 ∈ {1} → 𝑋 = 1) | 
| 19 | 18 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝑋 ∈ {1} → (𝑋↑𝑛) = (1↑𝑛)) | 
| 20 |  | nn0z 12638 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) | 
| 21 |  | 1exp 14132 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ →
(1↑𝑛) =
1) | 
| 22 | 20, 21 | syl 17 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ (1↑𝑛) =
1) | 
| 23 | 19, 22 | sylan9eq 2797 | . . . . . . . . 9
⊢ ((𝑋 ∈ {1} ∧ 𝑛 ∈ ℕ0)
→ (𝑋↑𝑛) = 1) | 
| 24 | 23 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝑋 ∈ {1} ∧ 𝑛 ∈ ℕ0)
→ ((𝐴‘𝑛) · (𝑋↑𝑛)) = ((𝐴‘𝑛) · 1)) | 
| 25 | 24 | mpteq2dva 5242 | . . . . . . 7
⊢ (𝑋 ∈ {1} → (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑋↑𝑛))) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · 1))) | 
| 26 | 25 | eqcomd 2743 | . . . . . 6
⊢ (𝑋 ∈ {1} → (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · 1)) = (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) | 
| 27 | 17, 26 | sylan9eq 2797 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ {1}) → 𝐴 = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) | 
| 28 | 27 | seqeq3d 14050 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ {1}) → seq0( + , 𝐴) = seq0( + , (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑋↑𝑛))))) | 
| 29 | 2 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ {1}) → seq0( + , 𝐴) ∈ dom ⇝
) | 
| 30 | 28, 29 | eqeltrrd 2842 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ {1}) → seq0( + , (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) ∈ dom ⇝ ) | 
| 31 |  | cnxmet 24793 | . . . . . . . 8
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) | 
| 32 |  | 0cn 11253 | . . . . . . . 8
⊢ 0 ∈
ℂ | 
| 33 |  | 1xr 11320 | . . . . . . . 8
⊢ 1 ∈
ℝ* | 
| 34 |  | blssm 24428 | . . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 1 ∈ ℝ*) → (0(ball‘(abs ∘ −
))1) ⊆ ℂ) | 
| 35 | 31, 32, 33, 34 | mp3an 1463 | . . . . . . 7
⊢
(0(ball‘(abs ∘ − ))1) ⊆ ℂ | 
| 36 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → 𝑋 ∈
(0(ball‘(abs ∘ − ))1)) | 
| 37 | 35, 36 | sselid 3981 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → 𝑋 ∈
ℂ) | 
| 38 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑧 = 𝑋 → (𝑧↑𝑛) = (𝑋↑𝑛)) | 
| 39 | 38 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑧 = 𝑋 → ((𝐴‘𝑛) · (𝑧↑𝑛)) = ((𝐴‘𝑛) · (𝑋↑𝑛))) | 
| 40 | 39 | mpteq2dv 5244 | . . . . . . 7
⊢ (𝑧 = 𝑋 → (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) | 
| 41 |  | eqid 2737 | . . . . . . 7
⊢ (𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑧↑𝑛)))) = (𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛)))) | 
| 42 |  | nn0ex 12532 | . . . . . . . 8
⊢
ℕ0 ∈ V | 
| 43 | 42 | mptex 7243 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑋↑𝑛))) ∈ V | 
| 44 | 40, 41, 43 | fvmpt 7016 | . . . . . 6
⊢ (𝑋 ∈ ℂ → ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑋) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) | 
| 45 | 37, 44 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → ((𝑧 ∈
ℂ ↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑋) = (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) | 
| 46 | 45 | seqeq3d 14050 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → seq0( + , ((𝑧
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑋)) = seq0( + , (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛))))) | 
| 47 | 1 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → 𝐴:ℕ0⟶ℂ) | 
| 48 |  | eqid 2737 | . . . . 5
⊢
sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) = sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) | 
| 49 | 37 | abscld 15475 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → (abs‘𝑋)
∈ ℝ) | 
| 50 | 49 | rexrd 11311 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → (abs‘𝑋)
∈ ℝ*) | 
| 51 |  | 1re 11261 | . . . . . . 7
⊢ 1 ∈
ℝ | 
| 52 |  | rexr 11307 | . . . . . . 7
⊢ (1 ∈
ℝ → 1 ∈ ℝ*) | 
| 53 | 51, 52 | mp1i 13 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → 1 ∈ ℝ*) | 
| 54 |  | iccssxr 13470 | . . . . . . 7
⊢
(0[,]+∞) ⊆ ℝ* | 
| 55 | 41, 47, 48 | radcnvcl 26460 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ (0[,]+∞)) | 
| 56 | 54, 55 | sselid 3981 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ*) | 
| 57 |  | eqid 2737 | . . . . . . . . . 10
⊢ (abs
∘ − ) = (abs ∘ − ) | 
| 58 | 57 | cnmetdval 24791 | . . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑋(abs
∘ − )0) = (abs‘(𝑋 − 0))) | 
| 59 | 37, 32, 58 | sylancl 586 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → (𝑋(abs ∘
− )0) = (abs‘(𝑋
− 0))) | 
| 60 | 37 | subid1d 11609 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → (𝑋 − 0)
= 𝑋) | 
| 61 | 60 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → (abs‘(𝑋
− 0)) = (abs‘𝑋)) | 
| 62 | 59, 61 | eqtrd 2777 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → (𝑋(abs ∘
− )0) = (abs‘𝑋)) | 
| 63 |  | elbl3 24402 | . . . . . . . . . 10
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (0 ∈ ℂ ∧ 𝑋 ∈ ℂ)) → (𝑋 ∈ (0(ball‘(abs ∘ −
))1) ↔ (𝑋(abs ∘
− )0) < 1)) | 
| 64 | 31, 33, 63 | mpanl12 702 | . . . . . . . . 9
⊢ ((0
∈ ℂ ∧ 𝑋
∈ ℂ) → (𝑋
∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) <
1)) | 
| 65 | 32, 37, 64 | sylancr 587 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → (𝑋 ∈
(0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) <
1)) | 
| 66 | 36, 65 | mpbid 232 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → (𝑋(abs ∘
− )0) < 1) | 
| 67 | 62, 66 | eqbrtrrd 5167 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → (abs‘𝑋)
< 1) | 
| 68 | 1, 2 | abelthlem1 26475 | . . . . . . 7
⊢ (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑧 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) | 
| 69 | 68 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → 1 ≤ sup({𝑟
∈ ℝ ∣ seq0( + , ((𝑧 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) | 
| 70 | 50, 53, 56, 67, 69 | xrltletrd 13203 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → (abs‘𝑋)
< sup({𝑟 ∈ ℝ
∣ seq0( + , ((𝑧
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) | 
| 71 | 41, 47, 48, 37, 70 | radcnvlt2 26462 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → seq0( + , ((𝑧
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑧↑𝑛))))‘𝑋)) ∈ dom ⇝ ) | 
| 72 | 46, 71 | eqeltrrd 2842 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → seq0( + , (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) ∈ dom ⇝ ) | 
| 73 | 30, 72 | jaodan 960 | . 2
⊢ ((𝜑 ∧ (𝑋 ∈ {1} ∨ 𝑋 ∈ (0(ball‘(abs ∘ −
))1))) → seq0( + , (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) ∈ dom ⇝ ) | 
| 74 | 12, 73 | syldan 591 | 1
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑆) → seq0( + , (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑋↑𝑛)))) ∈ dom ⇝ ) |