| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | geomulcvg.1 | . . . . . . 7
⊢ 𝐹 = (𝑘 ∈ ℕ0 ↦ (𝑘 · (𝐴↑𝑘))) | 
| 2 |  | elnn0 12528 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
↔ (𝑘 ∈ ℕ
∨ 𝑘 =
0)) | 
| 3 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → 𝐴 = 0) | 
| 4 | 3 | oveq1d 7446 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → (𝐴↑𝑘) = (0↑𝑘)) | 
| 5 |  | 0exp 14138 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ →
(0↑𝑘) =
0) | 
| 6 | 4, 5 | sylan9eq 2797 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) = 0) | 
| 7 | 6 | oveq2d 7447 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 ∈ ℕ) → (𝑘 · (𝐴↑𝑘)) = (𝑘 · 0)) | 
| 8 |  | nncn 12274 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) | 
| 9 | 8 | adantl 481 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
ℂ) | 
| 10 | 9 | mul01d 11460 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 ∈ ℕ) → (𝑘 · 0) =
0) | 
| 11 | 7, 10 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 ∈ ℕ) → (𝑘 · (𝐴↑𝑘)) = 0) | 
| 12 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 = 0) → 𝑘 = 0) | 
| 13 | 12 | oveq1d 7446 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 = 0) → (𝑘 · (𝐴↑𝑘)) = (0 · (𝐴↑𝑘))) | 
| 14 |  | simplll 775 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 = 0) → 𝐴 ∈ ℂ) | 
| 15 |  | 0nn0 12541 | . . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 | 
| 16 | 12, 15 | eqeltrdi 2849 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 = 0) → 𝑘 ∈ ℕ0) | 
| 17 | 14, 16 | expcld 14186 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 = 0) → (𝐴↑𝑘) ∈ ℂ) | 
| 18 | 17 | mul02d 11459 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 = 0) → (0 · (𝐴↑𝑘)) = 0) | 
| 19 | 13, 18 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 = 0) → (𝑘 · (𝐴↑𝑘)) = 0) | 
| 20 | 11, 19 | jaodan 960 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ (𝑘 ∈ ℕ ∨ 𝑘 = 0)) → (𝑘 · (𝐴↑𝑘)) = 0) | 
| 21 | 2, 20 | sylan2b 594 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 ∈ ℕ0)
→ (𝑘 · (𝐴↑𝑘)) = 0) | 
| 22 | 21 | mpteq2dva 5242 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → (𝑘 ∈ ℕ0
↦ (𝑘 · (𝐴↑𝑘))) = (𝑘 ∈ ℕ0 ↦
0)) | 
| 23 | 1, 22 | eqtrid 2789 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → 𝐹 = (𝑘 ∈ ℕ0 ↦
0)) | 
| 24 |  | fconstmpt 5747 | . . . . . . 7
⊢
(ℕ0 × {0}) = (𝑘 ∈ ℕ0 ↦
0) | 
| 25 |  | nn0uz 12920 | . . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) | 
| 26 | 25 | xpeq1i 5711 | . . . . . . 7
⊢
(ℕ0 × {0}) = ((ℤ≥‘0)
× {0}) | 
| 27 | 24, 26 | eqtr3i 2767 | . . . . . 6
⊢ (𝑘 ∈ ℕ0
↦ 0) = ((ℤ≥‘0) × {0}) | 
| 28 | 23, 27 | eqtrdi 2793 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → 𝐹 =
((ℤ≥‘0) × {0})) | 
| 29 | 28 | seqeq3d 14050 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → seq0( + ,
𝐹) = seq0( + ,
((ℤ≥‘0) × {0}))) | 
| 30 |  | 0z 12624 | . . . . 5
⊢ 0 ∈
ℤ | 
| 31 |  | serclim0 15613 | . . . . 5
⊢ (0 ∈
ℤ → seq0( + , ((ℤ≥‘0) × {0}))
⇝ 0) | 
| 32 | 30, 31 | ax-mp 5 | . . . 4
⊢ seq0( + ,
((ℤ≥‘0) × {0})) ⇝ 0 | 
| 33 | 29, 32 | eqbrtrdi 5182 | . . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → seq0( + ,
𝐹) ⇝
0) | 
| 34 |  | seqex 14044 | . . . 4
⊢ seq0( + ,
𝐹) ∈
V | 
| 35 |  | c0ex 11255 | . . . 4
⊢ 0 ∈
V | 
| 36 | 34, 35 | breldm 5919 | . . 3
⊢ (seq0( +
, 𝐹) ⇝ 0 → seq0(
+ , 𝐹) ∈ dom ⇝
) | 
| 37 | 33, 36 | syl 17 | . 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → seq0( + ,
𝐹) ∈ dom ⇝
) | 
| 38 |  | 1red 11262 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) → 1 ∈
ℝ) | 
| 39 |  | abscl 15317 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) | 
| 40 | 39 | adantr 480 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) ∈
ℝ) | 
| 41 |  | peano2re 11434 | . . . . . . . 8
⊢
((abs‘𝐴)
∈ ℝ → ((abs‘𝐴) + 1) ∈ ℝ) | 
| 42 | 40, 41 | syl 17 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ ((abs‘𝐴) + 1)
∈ ℝ) | 
| 43 | 42 | rehalfcld 12513 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (((abs‘𝐴) + 1)
/ 2) ∈ ℝ) | 
| 44 | 43 | adantr 480 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) →
(((abs‘𝐴) + 1) / 2)
∈ ℝ) | 
| 45 |  | absrpcl 15327 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) | 
| 46 | 45 | adantlr 715 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) →
(abs‘𝐴) ∈
ℝ+) | 
| 47 | 44, 46 | rerpdivcld 13108 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) →
((((abs‘𝐴) + 1) / 2)
/ (abs‘𝐴)) ∈
ℝ) | 
| 48 | 40 | recnd 11289 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) ∈
ℂ) | 
| 49 | 48 | mullidd 11279 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (1 · (abs‘𝐴)) = (abs‘𝐴)) | 
| 50 |  | simpr 484 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) <
1) | 
| 51 |  | 1re 11261 | . . . . . . . . 9
⊢ 1 ∈
ℝ | 
| 52 |  | avglt1 12504 | . . . . . . . . 9
⊢
(((abs‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝐴) < 1 ↔ (abs‘𝐴) < (((abs‘𝐴) + 1) / 2))) | 
| 53 | 40, 51, 52 | sylancl 586 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ ((abs‘𝐴) <
1 ↔ (abs‘𝐴) <
(((abs‘𝐴) + 1) /
2))) | 
| 54 | 50, 53 | mpbid 232 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) <
(((abs‘𝐴) + 1) /
2)) | 
| 55 | 49, 54 | eqbrtrd 5165 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (1 · (abs‘𝐴)) < (((abs‘𝐴) + 1) / 2)) | 
| 56 | 55 | adantr 480 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) → (1
· (abs‘𝐴))
< (((abs‘𝐴) + 1) /
2)) | 
| 57 | 38, 44, 46 | ltmuldivd 13124 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) → ((1
· (abs‘𝐴))
< (((abs‘𝐴) + 1) /
2) ↔ 1 < ((((abs‘𝐴) + 1) / 2) / (abs‘𝐴)))) | 
| 58 | 56, 57 | mpbid 232 | . . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) → 1 <
((((abs‘𝐴) + 1) / 2)
/ (abs‘𝐴))) | 
| 59 |  | expmulnbnd 14274 | . . . 4
⊢ ((1
∈ ℝ ∧ ((((abs‘𝐴) + 1) / 2) / (abs‘𝐴)) ∈ ℝ ∧ 1 <
((((abs‘𝐴) + 1) / 2)
/ (abs‘𝐴))) →
∃𝑛 ∈
ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑛)(1 · 𝑘) < (((((abs‘𝐴) + 1) / 2) / (abs‘𝐴))↑𝑘)) | 
| 60 | 38, 47, 58, 59 | syl3anc 1373 | . . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) →
∃𝑛 ∈
ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑛)(1 · 𝑘) < (((((abs‘𝐴) + 1) / 2) / (abs‘𝐴))↑𝑘)) | 
| 61 |  | eluznn0 12959 | . . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑛)) → 𝑘 ∈ ℕ0) | 
| 62 |  | nn0cn 12536 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) | 
| 63 | 62 | adantl 481 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℂ) | 
| 64 | 63 | mullidd 11279 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ (1 · 𝑘) =
𝑘) | 
| 65 | 43 | recnd 11289 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (((abs‘𝐴) + 1)
/ 2) ∈ ℂ) | 
| 66 | 65 | ad2antrr 726 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ (((abs‘𝐴) + 1)
/ 2) ∈ ℂ) | 
| 67 | 48 | ad2antrr 726 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ (abs‘𝐴) ∈
ℂ) | 
| 68 | 46 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ (abs‘𝐴) ∈
ℝ+) | 
| 69 | 68 | rpne0d 13082 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ (abs‘𝐴) ≠
0) | 
| 70 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℕ0) | 
| 71 | 66, 67, 69, 70 | expdivd 14200 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ (((((abs‘𝐴) +
1) / 2) / (abs‘𝐴))↑𝑘) = (((((abs‘𝐴) + 1) / 2)↑𝑘) / ((abs‘𝐴)↑𝑘))) | 
| 72 | 64, 71 | breq12d 5156 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ ((1 · 𝑘) <
(((((abs‘𝐴) + 1) / 2)
/ (abs‘𝐴))↑𝑘) ↔ 𝑘 < (((((abs‘𝐴) + 1) / 2)↑𝑘) / ((abs‘𝐴)↑𝑘)))) | 
| 73 |  | nn0re 12535 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) | 
| 74 | 73 | adantl 481 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℝ) | 
| 75 |  | reexpcl 14119 | . . . . . . . . . . 11
⊢
(((((abs‘𝐴) +
1) / 2) ∈ ℝ ∧ 𝑘 ∈ ℕ0) →
((((abs‘𝐴) + 1) /
2)↑𝑘) ∈
ℝ) | 
| 76 | 44, 75 | sylan 580 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ ((((abs‘𝐴) +
1) / 2)↑𝑘) ∈
ℝ) | 
| 77 | 40 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) →
(abs‘𝐴) ∈
ℝ) | 
| 78 |  | reexpcl 14119 | . . . . . . . . . . 11
⊢
(((abs‘𝐴)
∈ ℝ ∧ 𝑘
∈ ℕ0) → ((abs‘𝐴)↑𝑘) ∈ ℝ) | 
| 79 | 77, 78 | sylan 580 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ ((abs‘𝐴)↑𝑘) ∈ ℝ) | 
| 80 | 77 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ (abs‘𝐴) ∈
ℝ) | 
| 81 |  | nn0z 12638 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) | 
| 82 | 81 | adantl 481 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℤ) | 
| 83 | 68 | rpgt0d 13080 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ 0 < (abs‘𝐴)) | 
| 84 |  | expgt0 14136 | . . . . . . . . . . 11
⊢
(((abs‘𝐴)
∈ ℝ ∧ 𝑘
∈ ℤ ∧ 0 < (abs‘𝐴)) → 0 < ((abs‘𝐴)↑𝑘)) | 
| 85 | 80, 82, 83, 84 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ 0 < ((abs‘𝐴)↑𝑘)) | 
| 86 |  | ltmuldiv 12141 | . . . . . . . . . 10
⊢ ((𝑘 ∈ ℝ ∧
((((abs‘𝐴) + 1) /
2)↑𝑘) ∈ ℝ
∧ (((abs‘𝐴)↑𝑘) ∈ ℝ ∧ 0 <
((abs‘𝐴)↑𝑘))) → ((𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘) ↔ 𝑘 < (((((abs‘𝐴) + 1) / 2)↑𝑘) / ((abs‘𝐴)↑𝑘)))) | 
| 87 | 74, 76, 79, 85, 86 | syl112anc 1376 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑘 ·
((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘) ↔ 𝑘 < (((((abs‘𝐴) + 1) / 2)↑𝑘) / ((abs‘𝐴)↑𝑘)))) | 
| 88 | 72, 87 | bitr4d 282 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ ((1 · 𝑘) <
(((((abs‘𝐴) + 1) / 2)
/ (abs‘𝐴))↑𝑘) ↔ (𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) | 
| 89 | 61, 88 | sylan2 593 | . . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ (𝑛 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑛))) → ((1 · 𝑘) < (((((abs‘𝐴) + 1) / 2) / (abs‘𝐴))↑𝑘) ↔ (𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) | 
| 90 | 89 | anassrs 467 | . . . . . 6
⊢
(((((𝐴 ∈
ℂ ∧ (abs‘𝐴)
< 1) ∧ 𝐴 ≠ 0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((1 · 𝑘) < (((((abs‘𝐴) + 1) / 2) / (abs‘𝐴))↑𝑘) ↔ (𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) | 
| 91 | 90 | ralbidva 3176 | . . . . 5
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑛 ∈ ℕ0)
→ (∀𝑘 ∈
(ℤ≥‘𝑛)(1 · 𝑘) < (((((abs‘𝐴) + 1) / 2) / (abs‘𝐴))↑𝑘) ↔ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) | 
| 92 |  | simprl 771 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) → 𝑛 ∈ ℕ0) | 
| 93 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → ((((abs‘𝐴) + 1) / 2)↑𝑘) = ((((abs‘𝐴) + 1) / 2)↑𝑚)) | 
| 94 |  | eqid 2737 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
↦ ((((abs‘𝐴) +
1) / 2)↑𝑘)) = (𝑘 ∈ ℕ0
↦ ((((abs‘𝐴) +
1) / 2)↑𝑘)) | 
| 95 |  | ovex 7464 | . . . . . . . . . . 11
⊢
((((abs‘𝐴) +
1) / 2)↑𝑚) ∈
V | 
| 96 | 93, 94, 95 | fvmpt 7016 | . . . . . . . . . 10
⊢ (𝑚 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((((abs‘𝐴) + 1) / 2)↑𝑘))‘𝑚) = ((((abs‘𝐴) + 1) / 2)↑𝑚)) | 
| 97 | 96 | adantl 481 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((((abs‘𝐴) +
1) / 2)↑𝑘))‘𝑚) = ((((abs‘𝐴) + 1) / 2)↑𝑚)) | 
| 98 | 43 | ad2antrr 726 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) →
(((abs‘𝐴) + 1) / 2)
∈ ℝ) | 
| 99 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℕ0) | 
| 100 | 98, 99 | reexpcld 14203 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) →
((((abs‘𝐴) + 1) /
2)↑𝑚) ∈
ℝ) | 
| 101 | 97, 100 | eqeltrd 2841 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((((abs‘𝐴) +
1) / 2)↑𝑘))‘𝑚) ∈ ℝ) | 
| 102 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → 𝑘 = 𝑚) | 
| 103 |  | oveq2 7439 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (𝐴↑𝑘) = (𝐴↑𝑚)) | 
| 104 | 102, 103 | oveq12d 7449 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝑘 · (𝐴↑𝑘)) = (𝑚 · (𝐴↑𝑚))) | 
| 105 |  | ovex 7464 | . . . . . . . . . . 11
⊢ (𝑚 · (𝐴↑𝑚)) ∈ V | 
| 106 | 104, 1, 105 | fvmpt 7016 | . . . . . . . . . 10
⊢ (𝑚 ∈ ℕ0
→ (𝐹‘𝑚) = (𝑚 · (𝐴↑𝑚))) | 
| 107 | 106 | adantl 481 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → (𝐹‘𝑚) = (𝑚 · (𝐴↑𝑚))) | 
| 108 |  | nn0cn 12536 | . . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℂ) | 
| 109 | 108 | adantl 481 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℂ) | 
| 110 |  | expcl 14120 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑚 ∈ ℕ0)
→ (𝐴↑𝑚) ∈
ℂ) | 
| 111 | 110 | ad4ant14 752 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → (𝐴↑𝑚) ∈ ℂ) | 
| 112 | 109, 111 | mulcld 11281 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → (𝑚 · (𝐴↑𝑚)) ∈ ℂ) | 
| 113 | 107, 112 | eqeltrd 2841 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → (𝐹‘𝑚) ∈ ℂ) | 
| 114 |  | 0red 11264 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 0 ∈ ℝ) | 
| 115 |  | absge0 15326 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → 0 ≤
(abs‘𝐴)) | 
| 116 | 115 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 0 ≤ (abs‘𝐴)) | 
| 117 | 114, 40, 43, 116, 54 | lelttrd 11419 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 0 < (((abs‘𝐴) + 1) / 2)) | 
| 118 | 114, 43, 117 | ltled 11409 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 0 ≤ (((abs‘𝐴) + 1) / 2)) | 
| 119 | 43, 118 | absidd 15461 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘(((abs‘𝐴) + 1) / 2)) = (((abs‘𝐴) + 1) / 2)) | 
| 120 |  | avglt2 12505 | . . . . . . . . . . . . . 14
⊢
(((abs‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝐴) < 1 ↔ (((abs‘𝐴) + 1) / 2) <
1)) | 
| 121 | 40, 51, 120 | sylancl 586 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ ((abs‘𝐴) <
1 ↔ (((abs‘𝐴) +
1) / 2) < 1)) | 
| 122 | 50, 121 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (((abs‘𝐴) + 1)
/ 2) < 1) | 
| 123 | 119, 122 | eqbrtrd 5165 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘(((abs‘𝐴) + 1) / 2)) < 1) | 
| 124 |  | oveq2 7439 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → ((((abs‘𝐴) + 1) / 2)↑𝑘) = ((((abs‘𝐴) + 1) / 2)↑𝑛)) | 
| 125 |  | ovex 7464 | . . . . . . . . . . . . 13
⊢
((((abs‘𝐴) +
1) / 2)↑𝑛) ∈
V | 
| 126 | 124, 94, 125 | fvmpt 7016 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((((abs‘𝐴) + 1) / 2)↑𝑘))‘𝑛) = ((((abs‘𝐴) + 1) / 2)↑𝑛)) | 
| 127 | 126 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((𝑘 ∈ ℕ0 ↦
((((abs‘𝐴) + 1) /
2)↑𝑘))‘𝑛) = ((((abs‘𝐴) + 1) / 2)↑𝑛)) | 
| 128 | 65, 123, 127 | geolim 15906 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑘 ∈
ℕ0 ↦ ((((abs‘𝐴) + 1) / 2)↑𝑘))) ⇝ (1 / (1 −
(((abs‘𝐴) + 1) /
2)))) | 
| 129 |  | seqex 14044 | . . . . . . . . . . 11
⊢ seq0( + ,
(𝑘 ∈
ℕ0 ↦ ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∈ V | 
| 130 |  | ovex 7464 | . . . . . . . . . . 11
⊢ (1 / (1
− (((abs‘𝐴) +
1) / 2))) ∈ V | 
| 131 | 129, 130 | breldm 5919 | . . . . . . . . . 10
⊢ (seq0( +
, (𝑘 ∈
ℕ0 ↦ ((((abs‘𝐴) + 1) / 2)↑𝑘))) ⇝ (1 / (1 −
(((abs‘𝐴) + 1) / 2)))
→ seq0( + , (𝑘 ∈
ℕ0 ↦ ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∈ dom ⇝ ) | 
| 132 | 128, 131 | syl 17 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑘 ∈
ℕ0 ↦ ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∈ dom ⇝ ) | 
| 133 | 132 | adantr 480 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) → seq0( + , (𝑘 ∈ ℕ0 ↦
((((abs‘𝐴) + 1) /
2)↑𝑘))) ∈ dom
⇝ ) | 
| 134 |  | 1red 11262 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) → 1 ∈ ℝ) | 
| 135 |  | eluznn0 12959 | . . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ0
∧ 𝑚 ∈
(ℤ≥‘𝑛)) → 𝑚 ∈ ℕ0) | 
| 136 | 92, 135 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ ℕ0) | 
| 137 | 136 | nn0red 12588 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ ℝ) | 
| 138 |  | simplll 775 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝐴 ∈ ℂ) | 
| 139 | 138 | abscld 15475 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘𝐴) ∈
ℝ) | 
| 140 | 139, 136 | reexpcld 14203 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((abs‘𝐴)↑𝑚) ∈ ℝ) | 
| 141 | 137, 140 | remulcld 11291 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝑚 · ((abs‘𝐴)↑𝑚)) ∈ ℝ) | 
| 142 | 136, 100 | syldan 591 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((((abs‘𝐴) + 1) / 2)↑𝑚) ∈
ℝ) | 
| 143 |  | simprr 773 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) → ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘)) | 
| 144 |  | oveq2 7439 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑚 → ((abs‘𝐴)↑𝑘) = ((abs‘𝐴)↑𝑚)) | 
| 145 | 102, 144 | oveq12d 7449 | . . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → (𝑘 · ((abs‘𝐴)↑𝑘)) = (𝑚 · ((abs‘𝐴)↑𝑚))) | 
| 146 | 145, 93 | breq12d 5156 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → ((𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘) ↔ (𝑚 · ((abs‘𝐴)↑𝑚)) < ((((abs‘𝐴) + 1) / 2)↑𝑚))) | 
| 147 | 146 | rspccva 3621 | . . . . . . . . . . . 12
⊢
((∀𝑘 ∈
(ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝑚 · ((abs‘𝐴)↑𝑚)) < ((((abs‘𝐴) + 1) / 2)↑𝑚)) | 
| 148 | 143, 147 | sylan 580 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝑚 · ((abs‘𝐴)↑𝑚)) < ((((abs‘𝐴) + 1) / 2)↑𝑚)) | 
| 149 | 141, 142,
148 | ltled 11409 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝑚 · ((abs‘𝐴)↑𝑚)) ≤ ((((abs‘𝐴) + 1) / 2)↑𝑚)) | 
| 150 | 136 | nn0cnd 12589 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ ℂ) | 
| 151 | 138, 136 | expcld 14186 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝐴↑𝑚) ∈ ℂ) | 
| 152 | 150, 151 | absmuld 15493 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘(𝑚 · (𝐴↑𝑚))) = ((abs‘𝑚) · (abs‘(𝐴↑𝑚)))) | 
| 153 | 136 | nn0ge0d 12590 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 0 ≤ 𝑚) | 
| 154 | 137, 153 | absidd 15461 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘𝑚) = 𝑚) | 
| 155 | 138, 136 | absexpd 15491 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘(𝐴↑𝑚)) = ((abs‘𝐴)↑𝑚)) | 
| 156 | 154, 155 | oveq12d 7449 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((abs‘𝑚) · (abs‘(𝐴↑𝑚))) = (𝑚 · ((abs‘𝐴)↑𝑚))) | 
| 157 | 152, 156 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘(𝑚 · (𝐴↑𝑚))) = (𝑚 · ((abs‘𝐴)↑𝑚))) | 
| 158 | 142 | recnd 11289 | . . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((((abs‘𝐴) + 1) / 2)↑𝑚) ∈
ℂ) | 
| 159 | 158 | mullidd 11279 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (1 ·
((((abs‘𝐴) + 1) /
2)↑𝑚)) =
((((abs‘𝐴) + 1) /
2)↑𝑚)) | 
| 160 | 149, 157,
159 | 3brtr4d 5175 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘(𝑚 · (𝐴↑𝑚))) ≤ (1 · ((((abs‘𝐴) + 1) / 2)↑𝑚))) | 
| 161 | 136, 106 | syl 17 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑚) = (𝑚 · (𝐴↑𝑚))) | 
| 162 | 161 | fveq2d 6910 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘(𝐹‘𝑚)) = (abs‘(𝑚 · (𝐴↑𝑚)))) | 
| 163 | 136, 96 | syl 17 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝑘 ∈ ℕ0 ↦
((((abs‘𝐴) + 1) /
2)↑𝑘))‘𝑚) = ((((abs‘𝐴) + 1) / 2)↑𝑚)) | 
| 164 | 163 | oveq2d 7447 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (1 · ((𝑘 ∈ ℕ0
↦ ((((abs‘𝐴) +
1) / 2)↑𝑘))‘𝑚)) = (1 · ((((abs‘𝐴) + 1) / 2)↑𝑚))) | 
| 165 | 160, 162,
164 | 3brtr4d 5175 | . . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘(𝐹‘𝑚)) ≤ (1 · ((𝑘 ∈ ℕ0 ↦
((((abs‘𝐴) + 1) /
2)↑𝑘))‘𝑚))) | 
| 166 | 25, 92, 101, 113, 133, 134, 165 | cvgcmpce 15854 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) → seq0( + , 𝐹) ∈ dom ⇝ ) | 
| 167 | 166 | expr 456 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘) → seq0( + , 𝐹) ∈ dom ⇝ )) | 
| 168 | 167 | adantlr 715 | . . . . 5
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑛 ∈ ℕ0)
→ (∀𝑘 ∈
(ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘) → seq0( + , 𝐹) ∈ dom ⇝ )) | 
| 169 | 91, 168 | sylbid 240 | . . . 4
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑛 ∈ ℕ0)
→ (∀𝑘 ∈
(ℤ≥‘𝑛)(1 · 𝑘) < (((((abs‘𝐴) + 1) / 2) / (abs‘𝐴))↑𝑘) → seq0( + , 𝐹) ∈ dom ⇝ )) | 
| 170 | 169 | rexlimdva 3155 | . . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) →
(∃𝑛 ∈
ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑛)(1 · 𝑘) < (((((abs‘𝐴) + 1) / 2) / (abs‘𝐴))↑𝑘) → seq0( + , 𝐹) ∈ dom ⇝ )) | 
| 171 | 60, 170 | mpd 15 | . 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) → seq0( + ,
𝐹) ∈ dom ⇝
) | 
| 172 | 37, 171 | pm2.61dane 3029 | 1
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , 𝐹) ∈
dom ⇝ ) |