Step | Hyp | Ref
| Expression |
1 | | nn0uz 11598 |
. 2
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 1nn0 11185 |
. . 3
⊢ 1 ∈
ℕ0 |
3 | 2 | a1i 11 |
. 2
⊢ (𝜑 → 1 ∈
ℕ0) |
4 | | id 22 |
. . . . . 6
⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘) |
5 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → ((𝐺‘𝑋)‘𝑚) = ((𝐺‘𝑋)‘𝑘)) |
6 | 5 | fveq2d 6107 |
. . . . . 6
⊢ (𝑚 = 𝑘 → (abs‘((𝐺‘𝑋)‘𝑚)) = (abs‘((𝐺‘𝑋)‘𝑘))) |
7 | 4, 6 | oveq12d 6567 |
. . . . 5
⊢ (𝑚 = 𝑘 → (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
8 | | eqid 2610 |
. . . . 5
⊢ (𝑚 ∈ ℕ0
↦ (𝑚 ·
(abs‘((𝐺‘𝑋)‘𝑚)))) = (𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚)))) |
9 | | ovex 6577 |
. . . . 5
⊢ (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))) ∈ V |
10 | 7, 8, 9 | fvmpt 6191 |
. . . 4
⊢ (𝑘 ∈ ℕ0
→ ((𝑚 ∈
ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))))‘𝑘) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
11 | 10 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑚 ∈ ℕ0
↦ (𝑚 ·
(abs‘((𝐺‘𝑋)‘𝑚))))‘𝑘) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
12 | | nn0re 11178 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
13 | 12 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈
ℝ) |
14 | | pser.g |
. . . . . . 7
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
15 | | radcnv.a |
. . . . . . 7
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
16 | | psergf.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℂ) |
17 | 14, 15, 16 | psergf 23970 |
. . . . . 6
⊢ (𝜑 → (𝐺‘𝑋):ℕ0⟶ℂ) |
18 | 17 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑋)‘𝑘) ∈ ℂ) |
19 | 18 | abscld 14023 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘((𝐺‘𝑋)‘𝑘)) ∈ ℝ) |
20 | 13, 19 | remulcld 9949 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))) ∈ ℝ) |
21 | 11, 20 | eqeltrd 2688 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑚 ∈ ℕ0
↦ (𝑚 ·
(abs‘((𝐺‘𝑋)‘𝑚))))‘𝑘) ∈ ℝ) |
22 | | fvco3 6185 |
. . . 4
⊢ (((𝐺‘𝑋):ℕ0⟶ℂ ∧
𝑘 ∈
ℕ0) → ((abs ∘ (𝐺‘𝑋))‘𝑘) = (abs‘((𝐺‘𝑋)‘𝑘))) |
23 | 17, 22 | sylan 487 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((abs
∘ (𝐺‘𝑋))‘𝑘) = (abs‘((𝐺‘𝑋)‘𝑘))) |
24 | 19 | recnd 9947 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘((𝐺‘𝑋)‘𝑘)) ∈ ℂ) |
25 | 23, 24 | eqeltrd 2688 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((abs
∘ (𝐺‘𝑋))‘𝑘) ∈ ℂ) |
26 | | radcnvlem2.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ ℂ) |
27 | | radcnvlem2.a |
. . 3
⊢ (𝜑 → (abs‘𝑋) < (abs‘𝑌)) |
28 | | radcnvlem2.c |
. . 3
⊢ (𝜑 → seq0( + , (𝐺‘𝑌)) ∈ dom ⇝ ) |
29 | 7 | cbvmptv 4678 |
. . 3
⊢ (𝑚 ∈ ℕ0
↦ (𝑚 ·
(abs‘((𝐺‘𝑋)‘𝑚)))) = (𝑘 ∈ ℕ0 ↦ (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
30 | 14, 15, 16, 26, 27, 28, 29 | radcnvlem1 23971 |
. 2
⊢ (𝜑 → seq0( + , (𝑚 ∈ ℕ0
↦ (𝑚 ·
(abs‘((𝐺‘𝑋)‘𝑚))))) ∈ dom ⇝ ) |
31 | | 1red 9934 |
. 2
⊢ (𝜑 → 1 ∈
ℝ) |
32 | | 1red 9934 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ 1 ∈ ℝ) |
33 | | elnnuz 11600 |
. . . . . 6
⊢ (𝑘 ∈ ℕ ↔ 𝑘 ∈
(ℤ≥‘1)) |
34 | | nnnn0 11176 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
35 | 33, 34 | sylbir 224 |
. . . . 5
⊢ (𝑘 ∈
(ℤ≥‘1) → 𝑘 ∈ ℕ0) |
36 | 35, 13 | sylan2 490 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ 𝑘 ∈
ℝ) |
37 | 35, 19 | sylan2 490 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (abs‘((𝐺‘𝑋)‘𝑘)) ∈ ℝ) |
38 | 18 | absge0d 14031 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 0 ≤
(abs‘((𝐺‘𝑋)‘𝑘))) |
39 | 35, 38 | sylan2 490 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ 0 ≤ (abs‘((𝐺‘𝑋)‘𝑘))) |
40 | | eluzle 11576 |
. . . . 5
⊢ (𝑘 ∈
(ℤ≥‘1) → 1 ≤ 𝑘) |
41 | 40 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ 1 ≤ 𝑘) |
42 | 32, 36, 37, 39, 41 | lemul1ad 10842 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (1 · (abs‘((𝐺‘𝑋)‘𝑘))) ≤ (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
43 | | absidm 13911 |
. . . . . 6
⊢ (((𝐺‘𝑋)‘𝑘) ∈ ℂ →
(abs‘(abs‘((𝐺‘𝑋)‘𝑘))) = (abs‘((𝐺‘𝑋)‘𝑘))) |
44 | 18, 43 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘(abs‘((𝐺‘𝑋)‘𝑘))) = (abs‘((𝐺‘𝑋)‘𝑘))) |
45 | 23 | fveq2d 6107 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘((abs ∘ (𝐺‘𝑋))‘𝑘)) = (abs‘(abs‘((𝐺‘𝑋)‘𝑘)))) |
46 | 24 | mulid2d 9937 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1
· (abs‘((𝐺‘𝑋)‘𝑘))) = (abs‘((𝐺‘𝑋)‘𝑘))) |
47 | 44, 45, 46 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(abs‘((abs ∘ (𝐺‘𝑋))‘𝑘)) = (1 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
48 | 35, 47 | sylan2 490 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (abs‘((abs ∘ (𝐺‘𝑋))‘𝑘)) = (1 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
49 | 11 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1
· ((𝑚 ∈
ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))))‘𝑘)) = (1 · (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))))) |
50 | 20 | recnd 9947 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘))) ∈ ℂ) |
51 | 50 | mulid2d 9937 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1
· (𝑘 ·
(abs‘((𝐺‘𝑋)‘𝑘)))) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
52 | 49, 51 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1
· ((𝑚 ∈
ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))))‘𝑘)) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
53 | 35, 52 | sylan2 490 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (1 · ((𝑚
∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))))‘𝑘)) = (𝑘 · (abs‘((𝐺‘𝑋)‘𝑘)))) |
54 | 42, 48, 53 | 3brtr4d 4615 |
. 2
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘1))
→ (abs‘((abs ∘ (𝐺‘𝑋))‘𝑘)) ≤ (1 · ((𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))))‘𝑘))) |
55 | 1, 3, 21, 25, 30, 31, 54 | cvgcmpce 14391 |
1
⊢ (𝜑 → seq0( + , (abs ∘
(𝐺‘𝑋))) ∈ dom ⇝ ) |