| Step | Hyp | Ref
| Expression |
| 1 | | nn0uz 12920 |
. 2
⊢
ℕ0 = (ℤ≥‘0) |
| 2 | | 1nn0 12542 |
. . 3
⊢ 1 ∈
ℕ0 |
| 3 | 2 | a1i 11 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 1 ∈ ℕ0) |
| 4 | | oveq2 7439 |
. . . . 5
⊢ (𝑛 = 𝑘 → ((abs‘𝐴)↑𝑛) = ((abs‘𝐴)↑𝑘)) |
| 5 | | eqid 2737 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
↦ ((abs‘𝐴)↑𝑛)) = (𝑛 ∈ ℕ0 ↦
((abs‘𝐴)↑𝑛)) |
| 6 | | ovex 7464 |
. . . . 5
⊢
((abs‘𝐴)↑𝑘) ∈ V |
| 7 | 4, 5, 6 | fvmpt 7016 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘)) |
| 8 | 7 | adantl 481 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → ((𝑛 ∈ ℕ0 ↦
((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘)) |
| 9 | | abscl 15317 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
| 10 | 9 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) ∈
ℝ) |
| 11 | | reexpcl 14119 |
. . . 4
⊢
(((abs‘𝐴)
∈ ℝ ∧ 𝑘
∈ ℕ0) → ((abs‘𝐴)↑𝑘) ∈ ℝ) |
| 12 | 10, 11 | sylan 580 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → ((abs‘𝐴)↑𝑘) ∈ ℝ) |
| 13 | 8, 12 | eqeltrd 2841 |
. 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → ((𝑛 ∈ ℕ0 ↦
((abs‘𝐴)↑𝑛))‘𝑘) ∈ ℝ) |
| 14 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑛 = 0 ↔ 𝑘 = 0)) |
| 15 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘)) |
| 16 | 14, 15 | ifbieq2d 4552 |
. . . . . 6
⊢ (𝑛 = 𝑘 → if(𝑛 = 0, 0, (1 / 𝑛)) = if(𝑘 = 0, 0, (1 / 𝑘))) |
| 17 | | oveq2 7439 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (𝐴↑𝑛) = (𝐴↑𝑘)) |
| 18 | 16, 17 | oveq12d 7449 |
. . . . 5
⊢ (𝑛 = 𝑘 → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))) |
| 19 | | eqid 2737 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
↦ (if(𝑛 = 0, 0, (1 /
𝑛)) · (𝐴↑𝑛))) = (𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛))) |
| 20 | | ovex 7464 |
. . . . 5
⊢ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)) ∈ V |
| 21 | 18, 19, 20 | fvmpt 7016 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))) |
| 22 | 21 | adantl 481 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → ((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))) |
| 23 | | 0cnd 11254 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) ∧ 𝑘 = 0) → 0 ∈
ℂ) |
| 24 | | nn0cn 12536 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
| 25 | 24 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → 𝑘 ∈ ℂ) |
| 26 | | neqne 2948 |
. . . . . 6
⊢ (¬
𝑘 = 0 → 𝑘 ≠ 0) |
| 27 | | reccl 11929 |
. . . . . 6
⊢ ((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) → (1 / 𝑘) ∈
ℂ) |
| 28 | 25, 26, 27 | syl2an 596 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) ∧ ¬ 𝑘 = 0) → (1 / 𝑘) ∈ ℂ) |
| 29 | 23, 28 | ifclda 4561 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → if(𝑘 = 0, 0, (1 / 𝑘)) ∈ ℂ) |
| 30 | | expcl 14120 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) |
| 31 | 30 | adantlr 715 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → (𝐴↑𝑘) ∈ ℂ) |
| 32 | 29, 31 | mulcld 11281 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)) ∈ ℂ) |
| 33 | 22, 32 | eqeltrd 2841 |
. 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → ((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘) ∈ ℂ) |
| 34 | 10 | recnd 11289 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) ∈
ℂ) |
| 35 | | absidm 15362 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘(abs‘𝐴)) =
(abs‘𝐴)) |
| 36 | 35 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘(abs‘𝐴)) = (abs‘𝐴)) |
| 37 | | simpr 484 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) <
1) |
| 38 | 36, 37 | eqbrtrd 5165 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘(abs‘𝐴)) < 1) |
| 39 | 34, 38, 8 | geolim 15906 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑛 ∈
ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ⇝ (1 / (1 − (abs‘𝐴)))) |
| 40 | | seqex 14044 |
. . . 4
⊢ seq0( + ,
(𝑛 ∈
ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ∈ V |
| 41 | | ovex 7464 |
. . . 4
⊢ (1 / (1
− (abs‘𝐴)))
∈ V |
| 42 | 40, 41 | breldm 5919 |
. . 3
⊢ (seq0( +
, (𝑛 ∈
ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ⇝ (1 / (1 − (abs‘𝐴))) → seq0( + , (𝑛 ∈ ℕ0
↦ ((abs‘𝐴)↑𝑛))) ∈ dom ⇝ ) |
| 43 | 39, 42 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑛 ∈
ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ∈ dom ⇝ ) |
| 44 | | 1red 11262 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 1 ∈ ℝ) |
| 45 | | elnnuz 12922 |
. . 3
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) |
| 46 | | nnrecre 12308 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
| 47 | 46 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → (1
/ 𝑘) ∈
ℝ) |
| 48 | 47 | recnd 11289 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → (1
/ 𝑘) ∈
ℂ) |
| 49 | | nnnn0 12533 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
| 50 | 49, 31 | sylan2 593 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(𝐴↑𝑘) ∈ ℂ) |
| 51 | 48, 50 | absmuld 15493 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(abs‘((1 / 𝑘)
· (𝐴↑𝑘))) = ((abs‘(1 / 𝑘)) · (abs‘(𝐴↑𝑘)))) |
| 52 | | nnrp 13046 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
| 53 | 52 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
𝑘 ∈
ℝ+) |
| 54 | 53 | rpreccld 13087 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → (1
/ 𝑘) ∈
ℝ+) |
| 55 | 54 | rpge0d 13081 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → 0
≤ (1 / 𝑘)) |
| 56 | 47, 55 | absidd 15461 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(abs‘(1 / 𝑘)) = (1 /
𝑘)) |
| 57 | | simpl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 𝐴 ∈
ℂ) |
| 58 | | absexp 15343 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (abs‘(𝐴↑𝑘)) = ((abs‘𝐴)↑𝑘)) |
| 59 | 57, 49, 58 | syl2an 596 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(abs‘(𝐴↑𝑘)) = ((abs‘𝐴)↑𝑘)) |
| 60 | 56, 59 | oveq12d 7449 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
((abs‘(1 / 𝑘))
· (abs‘(𝐴↑𝑘))) = ((1 / 𝑘) · ((abs‘𝐴)↑𝑘))) |
| 61 | 51, 60 | eqtrd 2777 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(abs‘((1 / 𝑘)
· (𝐴↑𝑘))) = ((1 / 𝑘) · ((abs‘𝐴)↑𝑘))) |
| 62 | | 1red 11262 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → 1
∈ ℝ) |
| 63 | 49, 12 | sylan2 593 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
((abs‘𝐴)↑𝑘) ∈
ℝ) |
| 64 | 50 | absge0d 15483 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → 0
≤ (abs‘(𝐴↑𝑘))) |
| 65 | 64, 59 | breqtrd 5169 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → 0
≤ ((abs‘𝐴)↑𝑘)) |
| 66 | | nnge1 12294 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 1 ≤
𝑘) |
| 67 | 66 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → 1
≤ 𝑘) |
| 68 | | 0lt1 11785 |
. . . . . . . . . 10
⊢ 0 <
1 |
| 69 | 68 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → 0
< 1) |
| 70 | | nnre 12273 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
| 71 | 70 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
𝑘 ∈
ℝ) |
| 72 | | nngt0 12297 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 0 <
𝑘) |
| 73 | 72 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → 0
< 𝑘) |
| 74 | | lerec 12151 |
. . . . . . . . 9
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → (1 ≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 / 1))) |
| 75 | 62, 69, 71, 73, 74 | syl22anc 839 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → (1
≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 /
1))) |
| 76 | 67, 75 | mpbid 232 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → (1
/ 𝑘) ≤ (1 /
1)) |
| 77 | | 1div1e1 11958 |
. . . . . . 7
⊢ (1 / 1) =
1 |
| 78 | 76, 77 | breqtrdi 5184 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → (1
/ 𝑘) ≤
1) |
| 79 | 47, 62, 63, 65, 78 | lemul1ad 12207 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
((1 / 𝑘) ·
((abs‘𝐴)↑𝑘)) ≤ (1 ·
((abs‘𝐴)↑𝑘))) |
| 80 | 61, 79 | eqbrtrd 5165 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(abs‘((1 / 𝑘)
· (𝐴↑𝑘))) ≤ (1 ·
((abs‘𝐴)↑𝑘))) |
| 81 | 49, 22 | sylan2 593 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
((𝑛 ∈
ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))) |
| 82 | | nnne0 12300 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
| 83 | 82 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
𝑘 ≠ 0) |
| 84 | 83 | neneqd 2945 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
¬ 𝑘 =
0) |
| 85 | 84 | iffalsed 4536 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
if(𝑘 = 0, 0, (1 / 𝑘)) = (1 / 𝑘)) |
| 86 | 85 | oveq1d 7446 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)) = ((1 / 𝑘) · (𝐴↑𝑘))) |
| 87 | 81, 86 | eqtrd 2777 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
((𝑛 ∈
ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘) = ((1 / 𝑘) · (𝐴↑𝑘))) |
| 88 | 87 | fveq2d 6910 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(abs‘((𝑛 ∈
ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘)) = (abs‘((1 / 𝑘) · (𝐴↑𝑘)))) |
| 89 | 49, 8 | sylan2 593 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
((𝑛 ∈
ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘)) |
| 90 | 89 | oveq2d 7447 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → (1
· ((𝑛 ∈
ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘)) = (1 · ((abs‘𝐴)↑𝑘))) |
| 91 | 80, 88, 90 | 3brtr4d 5175 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(abs‘((𝑛 ∈
ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘)) ≤ (1 · ((𝑛 ∈ ℕ0 ↦
((abs‘𝐴)↑𝑛))‘𝑘))) |
| 92 | 45, 91 | sylan2br 595 |
. 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
(ℤ≥‘1)) → (abs‘((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘)) ≤ (1 · ((𝑛 ∈ ℕ0 ↦
((abs‘𝐴)↑𝑛))‘𝑘))) |
| 93 | 1, 3, 13, 33, 43, 44, 92 | cvgcmpce 15854 |
1
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑛 ∈
ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))) ∈ dom ⇝ ) |