Step | Hyp | Ref
| Expression |
1 | | nn0uz 12004 |
. 2
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 1nn0 11636 |
. . 3
⊢ 1 ∈
ℕ0 |
3 | 2 | a1i 11 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 1 ∈ ℕ0) |
4 | | oveq2 6913 |
. . . . 5
⊢ (𝑛 = 𝑘 → ((abs‘𝐴)↑𝑛) = ((abs‘𝐴)↑𝑘)) |
5 | | eqid 2825 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
↦ ((abs‘𝐴)↑𝑛)) = (𝑛 ∈ ℕ0 ↦
((abs‘𝐴)↑𝑛)) |
6 | | ovex 6937 |
. . . . 5
⊢
((abs‘𝐴)↑𝑘) ∈ V |
7 | 4, 5, 6 | fvmpt 6529 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘)) |
8 | 7 | adantl 475 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → ((𝑛 ∈ ℕ0 ↦
((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘)) |
9 | | abscl 14395 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
10 | 9 | adantr 474 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) ∈
ℝ) |
11 | | reexpcl 13171 |
. . . 4
⊢
(((abs‘𝐴)
∈ ℝ ∧ 𝑘
∈ ℕ0) → ((abs‘𝐴)↑𝑘) ∈ ℝ) |
12 | 10, 11 | sylan 577 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → ((abs‘𝐴)↑𝑘) ∈ ℝ) |
13 | 8, 12 | eqeltrd 2906 |
. 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → ((𝑛 ∈ ℕ0 ↦
((abs‘𝐴)↑𝑛))‘𝑘) ∈ ℝ) |
14 | | eqeq1 2829 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑛 = 0 ↔ 𝑘 = 0)) |
15 | | oveq2 6913 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘)) |
16 | 14, 15 | ifbieq2d 4331 |
. . . . . 6
⊢ (𝑛 = 𝑘 → if(𝑛 = 0, 0, (1 / 𝑛)) = if(𝑘 = 0, 0, (1 / 𝑘))) |
17 | | oveq2 6913 |
. . . . . 6
⊢ (𝑛 = 𝑘 → (𝐴↑𝑛) = (𝐴↑𝑘)) |
18 | 16, 17 | oveq12d 6923 |
. . . . 5
⊢ (𝑛 = 𝑘 → (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))) |
19 | | eqid 2825 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
↦ (if(𝑛 = 0, 0, (1 /
𝑛)) · (𝐴↑𝑛))) = (𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛))) |
20 | | ovex 6937 |
. . . . 5
⊢ (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)) ∈ V |
21 | 18, 19, 20 | fvmpt 6529 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))) |
22 | 21 | adantl 475 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → ((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))) |
23 | | 0cnd 10349 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) ∧ 𝑘 = 0) → 0 ∈
ℂ) |
24 | | nn0cn 11629 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
25 | 24 | adantl 475 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → 𝑘 ∈ ℂ) |
26 | | df-ne 3000 |
. . . . . . 7
⊢ (𝑘 ≠ 0 ↔ ¬ 𝑘 = 0) |
27 | 26 | biimpri 220 |
. . . . . 6
⊢ (¬
𝑘 = 0 → 𝑘 ≠ 0) |
28 | | reccl 11017 |
. . . . . 6
⊢ ((𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) → (1 / 𝑘) ∈
ℂ) |
29 | 25, 27, 28 | syl2an 591 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) ∧ ¬ 𝑘 = 0) → (1 / 𝑘) ∈ ℂ) |
30 | 23, 29 | ifclda 4340 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → if(𝑘 = 0, 0, (1 / 𝑘)) ∈ ℂ) |
31 | | expcl 13172 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) |
32 | 31 | adantlr 708 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → (𝐴↑𝑘) ∈ ℂ) |
33 | 30, 32 | mulcld 10377 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)) ∈ ℂ) |
34 | 22, 33 | eqeltrd 2906 |
. 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
ℕ0) → ((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘) ∈ ℂ) |
35 | 10 | recnd 10385 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) ∈
ℂ) |
36 | | absidm 14440 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘(abs‘𝐴)) =
(abs‘𝐴)) |
37 | 36 | adantr 474 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘(abs‘𝐴)) = (abs‘𝐴)) |
38 | | simpr 479 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) <
1) |
39 | 37, 38 | eqbrtrd 4895 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘(abs‘𝐴)) < 1) |
40 | 35, 39, 8 | geolim 14975 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑛 ∈
ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ⇝ (1 / (1 − (abs‘𝐴)))) |
41 | | seqex 13097 |
. . . 4
⊢ seq0( + ,
(𝑛 ∈
ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ∈ V |
42 | | ovex 6937 |
. . . 4
⊢ (1 / (1
− (abs‘𝐴)))
∈ V |
43 | 41, 42 | breldm 5561 |
. . 3
⊢ (seq0( +
, (𝑛 ∈
ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ⇝ (1 / (1 − (abs‘𝐴))) → seq0( + , (𝑛 ∈ ℕ0
↦ ((abs‘𝐴)↑𝑛))) ∈ dom ⇝ ) |
44 | 40, 43 | syl 17 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑛 ∈
ℕ0 ↦ ((abs‘𝐴)↑𝑛))) ∈ dom ⇝ ) |
45 | | 1red 10357 |
. 2
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 1 ∈ ℝ) |
46 | | elnnuz 12006 |
. . 3
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) |
47 | | nnrecre 11393 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
48 | 47 | adantl 475 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → (1
/ 𝑘) ∈
ℝ) |
49 | 48 | recnd 10385 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → (1
/ 𝑘) ∈
ℂ) |
50 | | nnnn0 11626 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
51 | 50, 32 | sylan2 588 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(𝐴↑𝑘) ∈ ℂ) |
52 | 49, 51 | absmuld 14570 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(abs‘((1 / 𝑘)
· (𝐴↑𝑘))) = ((abs‘(1 / 𝑘)) · (abs‘(𝐴↑𝑘)))) |
53 | | nnrp 12125 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
54 | 53 | adantl 475 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
𝑘 ∈
ℝ+) |
55 | 54 | rpreccld 12166 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → (1
/ 𝑘) ∈
ℝ+) |
56 | 55 | rpge0d 12160 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → 0
≤ (1 / 𝑘)) |
57 | 48, 56 | absidd 14538 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(abs‘(1 / 𝑘)) = (1 /
𝑘)) |
58 | | simpl 476 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 𝐴 ∈
ℂ) |
59 | | absexp 14421 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (abs‘(𝐴↑𝑘)) = ((abs‘𝐴)↑𝑘)) |
60 | 58, 50, 59 | syl2an 591 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(abs‘(𝐴↑𝑘)) = ((abs‘𝐴)↑𝑘)) |
61 | 57, 60 | oveq12d 6923 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
((abs‘(1 / 𝑘))
· (abs‘(𝐴↑𝑘))) = ((1 / 𝑘) · ((abs‘𝐴)↑𝑘))) |
62 | 52, 61 | eqtrd 2861 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(abs‘((1 / 𝑘)
· (𝐴↑𝑘))) = ((1 / 𝑘) · ((abs‘𝐴)↑𝑘))) |
63 | | 1red 10357 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → 1
∈ ℝ) |
64 | 50, 12 | sylan2 588 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
((abs‘𝐴)↑𝑘) ∈
ℝ) |
65 | 51 | absge0d 14560 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → 0
≤ (abs‘(𝐴↑𝑘))) |
66 | 65, 60 | breqtrd 4899 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → 0
≤ ((abs‘𝐴)↑𝑘)) |
67 | | nnge1 11380 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 1 ≤
𝑘) |
68 | 67 | adantl 475 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → 1
≤ 𝑘) |
69 | | 0lt1 10874 |
. . . . . . . . . 10
⊢ 0 <
1 |
70 | 69 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → 0
< 1) |
71 | | nnre 11358 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
72 | 71 | adantl 475 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
𝑘 ∈
ℝ) |
73 | | nngt0 11383 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 0 <
𝑘) |
74 | 73 | adantl 475 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → 0
< 𝑘) |
75 | | lerec 11236 |
. . . . . . . . 9
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → (1 ≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 / 1))) |
76 | 63, 70, 72, 74, 75 | syl22anc 874 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → (1
≤ 𝑘 ↔ (1 / 𝑘) ≤ (1 /
1))) |
77 | 68, 76 | mpbid 224 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → (1
/ 𝑘) ≤ (1 /
1)) |
78 | | 1div1e1 11042 |
. . . . . . 7
⊢ (1 / 1) =
1 |
79 | 77, 78 | syl6breq 4914 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → (1
/ 𝑘) ≤
1) |
80 | 48, 63, 64, 66, 79 | lemul1ad 11293 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
((1 / 𝑘) ·
((abs‘𝐴)↑𝑘)) ≤ (1 ·
((abs‘𝐴)↑𝑘))) |
81 | 62, 80 | eqbrtrd 4895 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(abs‘((1 / 𝑘)
· (𝐴↑𝑘))) ≤ (1 ·
((abs‘𝐴)↑𝑘))) |
82 | 50, 22 | sylan2 588 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
((𝑛 ∈
ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘) = (if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘))) |
83 | | nnne0 11386 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
84 | 83 | adantl 475 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
𝑘 ≠ 0) |
85 | 84 | neneqd 3004 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
¬ 𝑘 =
0) |
86 | 85 | iffalsed 4317 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
if(𝑘 = 0, 0, (1 / 𝑘)) = (1 / 𝑘)) |
87 | 86 | oveq1d 6920 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(if(𝑘 = 0, 0, (1 / 𝑘)) · (𝐴↑𝑘)) = ((1 / 𝑘) · (𝐴↑𝑘))) |
88 | 82, 87 | eqtrd 2861 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
((𝑛 ∈
ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘) = ((1 / 𝑘) · (𝐴↑𝑘))) |
89 | 88 | fveq2d 6437 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(abs‘((𝑛 ∈
ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘)) = (abs‘((1 / 𝑘) · (𝐴↑𝑘)))) |
90 | 50, 8 | sylan2 588 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
((𝑛 ∈
ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘) = ((abs‘𝐴)↑𝑘)) |
91 | 90 | oveq2d 6921 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) → (1
· ((𝑛 ∈
ℕ0 ↦ ((abs‘𝐴)↑𝑛))‘𝑘)) = (1 · ((abs‘𝐴)↑𝑘))) |
92 | 81, 89, 91 | 3brtr4d 4905 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈ ℕ) →
(abs‘((𝑛 ∈
ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘)) ≤ (1 · ((𝑛 ∈ ℕ0 ↦
((abs‘𝐴)↑𝑛))‘𝑘))) |
93 | 46, 92 | sylan2br 590 |
. 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑘 ∈
(ℤ≥‘1)) → (abs‘((𝑛 ∈ ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))‘𝑘)) ≤ (1 · ((𝑛 ∈ ℕ0 ↦
((abs‘𝐴)↑𝑛))‘𝑘))) |
94 | 1, 3, 13, 34, 44, 45, 93 | cvgcmpce 14924 |
1
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑛 ∈
ℕ0 ↦ (if(𝑛 = 0, 0, (1 / 𝑛)) · (𝐴↑𝑛)))) ∈ dom ⇝ ) |