Step | Hyp | Ref
| Expression |
1 | | nn0uz 12602 |
. 2
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 1nn0 12232 |
. . 3
⊢ 1 ∈
ℕ0 |
3 | 2 | a1i 11 |
. 2
⊢ (𝜑 → 1 ∈
ℕ0) |
4 | | id 22 |
. . . . . 6
⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘) |
5 | | 2fveq3 6773 |
. . . . . 6
⊢ (𝑚 = 𝑘 → (abs‘((𝐺‘𝑋)‘𝑚)) = (abs‘((𝐺‘𝑋)‘𝑘))) |
6 | 4, 5 | oveq12d 7286 |
. . . . 5
⊢ (𝑚 = 𝑘 → (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
7 | | eqid 2739 |
. . . . 5
⊢ (𝑚 ∈ ℕ0
↦ (𝑚 ·
(abs‘((𝐺‘𝑋)‘𝑚)))) = (𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚)))) |
8 | | ovex 7301 |
. . . . 5
⊢ (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))) ∈ V |
9 | 6, 7, 8 | fvmpt 6869 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ ((𝑚 ∈
ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))))‘𝑘) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
10 | 9 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑚 ∈ ℕ0
↦ (𝑚 ·
(abs‘((𝐺‘𝑋)‘𝑚))))‘𝑘) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
11 | | nn0re 12225 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
12 | 11 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℝ) |
13 | | pser.g |
. . . . . . 7
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
14 | | radcnv.a |
. . . . . . 7
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
15 | | psergf.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℂ) |
16 | 13, 14, 15 | psergf 25552 |
. . . . . 6
⊢ (𝜑 → (𝐺‘𝑋):ℕ0⟶ℂ) |
17 | 16 | ffvelrnda 6955 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑋)‘𝑘) ∈ ℂ) |
18 | 17 | abscld 15129 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘((𝐺‘𝑋)‘𝑘)) ∈ ℝ) |
19 | 12, 18 | remulcld 10989 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))) ∈ ℝ) |
20 | 10, 19 | eqeltrd 2840 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑚 ∈ ℕ0
↦ (𝑚 ·
(abs‘((𝐺‘𝑋)‘𝑚))))‘𝑘) ∈ ℝ) |
21 | | fvco3 6861 |
. . . 4
⊢ (((𝐺‘𝑋):ℕ0⟶ℂ ∧
𝑘 ∈
ℕ0) → ((abs ∘ (𝐺‘𝑋))‘𝑘) = (abs‘((𝐺‘𝑋)‘𝑘))) |
22 | 16, 21 | sylan 579 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((abs
∘ (𝐺‘𝑋))‘𝑘) = (abs‘((𝐺‘𝑋)‘𝑘))) |
23 | 18 | recnd 10987 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘((𝐺‘𝑋)‘𝑘)) ∈ ℂ) |
24 | 22, 23 | eqeltrd 2840 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((abs
∘ (𝐺‘𝑋))‘𝑘) ∈ ℂ) |
25 | | radcnvlem2.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ ℂ) |
26 | | radcnvlem2.a |
. . 3
⊢ (𝜑 → (abs‘𝑋) < (abs‘𝑌)) |
27 | | radcnvlem2.c |
. . 3
⊢ (𝜑 → seq0( + , (𝐺‘𝑌)) ∈ dom ⇝ ) |
28 | 6 | cbvmptv 5191 |
. . 3
⊢ (𝑚 ∈ ℕ0
↦ (𝑚 ·
(abs‘((𝐺‘𝑋)‘𝑚)))) = (𝑘 ∈ ℕ0 ↦ (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
29 | 13, 14, 15, 25, 26, 27, 28 | radcnvlem1 25553 |
. 2
⊢ (𝜑 → seq0( + , (𝑚 ∈ ℕ0
↦ (𝑚 ·
(abs‘((𝐺‘𝑋)‘𝑚))))) ∈ dom ⇝ ) |
30 | | 1red 10960 |
. 2
⊢ (𝜑 → 1 ∈
ℝ) |
31 | | 1red 10960 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ 1 ∈ ℝ) |
32 | | elnnuz 12604 |
. . . . . 6
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) |
33 | | nnnn0 12223 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
34 | 32, 33 | sylbir 234 |
. . . . 5
⊢ (𝑘 ∈
(ℤ≥‘1) → 𝑘 ∈ ℕ0) |
35 | 34, 12 | sylan2 592 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ 𝑘 ∈
ℝ) |
36 | 34, 18 | sylan2 592 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (abs‘((𝐺‘𝑋)‘𝑘)) ∈ ℝ) |
37 | 17 | absge0d 15137 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤
(abs‘((𝐺‘𝑋)‘𝑘))) |
38 | 34, 37 | sylan2 592 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ 0 ≤ (abs‘((𝐺‘𝑋)‘𝑘))) |
39 | | eluzle 12577 |
. . . . 5
⊢ (𝑘 ∈
(ℤ≥‘1) → 1 ≤ 𝑘) |
40 | 39 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ 1 ≤ 𝑘) |
41 | 31, 35, 36, 38, 40 | lemul1ad 11897 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (1 · (abs‘((𝐺‘𝑋)‘𝑘))) ≤ (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
42 | | absidm 15016 |
. . . . . 6
⊢ (((𝐺‘𝑋)‘𝑘) ∈ ℂ →
(abs‘(abs‘((𝐺‘𝑋)‘𝑘))) = (abs‘((𝐺‘𝑋)‘𝑘))) |
43 | 17, 42 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘(abs‘((𝐺‘𝑋)‘𝑘))) = (abs‘((𝐺‘𝑋)‘𝑘))) |
44 | 22 | fveq2d 6772 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘((abs ∘ (𝐺‘𝑋))‘𝑘)) = (abs‘(abs‘((𝐺‘𝑋)‘𝑘)))) |
45 | 23 | mulid2d 10977 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1
· (abs‘((𝐺‘𝑋)‘𝑘))) = (abs‘((𝐺‘𝑋)‘𝑘))) |
46 | 43, 44, 45 | 3eqtr4d 2789 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘((abs ∘ (𝐺‘𝑋))‘𝑘)) = (1 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
47 | 34, 46 | sylan2 592 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (abs‘((abs ∘ (𝐺‘𝑋))‘𝑘)) = (1 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
48 | 10 | oveq2d 7284 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1
· ((𝑚 ∈
ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))))‘𝑘)) = (1 · (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))))) |
49 | 19 | recnd 10987 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))) ∈ ℂ) |
50 | 49 | mulid2d 10977 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1
· (𝑘 ·
(abs‘((𝐺‘𝑋)‘𝑘)))) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
51 | 48, 50 | eqtrd 2779 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1
· ((𝑚 ∈
ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))))‘𝑘)) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
52 | 34, 51 | sylan2 592 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (1 · ((𝑚
∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))))‘𝑘)) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
53 | 41, 47, 52 | 3brtr4d 5110 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (abs‘((abs ∘ (𝐺‘𝑋))‘𝑘)) ≤ (1 · ((𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))))‘𝑘))) |
54 | 1, 3, 20, 24, 29, 30, 53 | cvgcmpce 15511 |
1
⊢ (𝜑 → seq0( + , (abs ∘
(𝐺‘𝑋))) ∈ dom ⇝ ) |