Step |
Hyp |
Ref |
Expression |
1 |
|
pser.g |
⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ) |
2 |
|
radcnv.a |
⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ ) |
3 |
|
psergf.x |
⊢ ( 𝜑 → 𝑋 ∈ ℂ ) |
4 |
|
radcnvlem2.y |
⊢ ( 𝜑 → 𝑌 ∈ ℂ ) |
5 |
|
radcnvlem2.a |
⊢ ( 𝜑 → ( abs ‘ 𝑋 ) < ( abs ‘ 𝑌 ) ) |
6 |
|
radcnvlem2.c |
⊢ ( 𝜑 → seq 0 ( + , ( 𝐺 ‘ 𝑌 ) ) ∈ dom ⇝ ) |
7 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
8 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
9 |
8
|
a1i |
⊢ ( 𝜑 → 1 ∈ ℕ0 ) |
10 |
|
id |
⊢ ( 𝑚 = 𝑘 → 𝑚 = 𝑘 ) |
11 |
|
2fveq3 |
⊢ ( 𝑚 = 𝑘 → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) |
12 |
10 11
|
oveq12d |
⊢ ( 𝑚 = 𝑘 → ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) = ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ) |
13 |
|
eqid |
⊢ ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) = ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) |
14 |
|
ovex |
⊢ ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ∈ V |
15 |
12 13 14
|
fvmpt |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) = ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ) |
16 |
15
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) = ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ) |
17 |
|
nn0re |
⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ ) |
18 |
17
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℝ ) |
19 |
1 2 3
|
psergf |
⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) : ℕ0 ⟶ ℂ ) |
20 |
19
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ∈ ℂ ) |
21 |
20
|
abscld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ∈ ℝ ) |
22 |
18 21
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ∈ ℝ ) |
23 |
16 22
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ∈ ℝ ) |
24 |
|
fvco3 |
⊢ ( ( ( 𝐺 ‘ 𝑋 ) : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ‘ 𝑘 ) = ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) |
25 |
19 24
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ‘ 𝑘 ) = ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) |
26 |
21
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ∈ ℂ ) |
27 |
25 26
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ‘ 𝑘 ) ∈ ℂ ) |
28 |
12
|
cbvmptv |
⊢ ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ) |
29 |
1 2 3 4 5 6 28
|
radcnvlem1 |
⊢ ( 𝜑 → seq 0 ( + , ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) ) ∈ dom ⇝ ) |
30 |
|
1red |
⊢ ( 𝜑 → 1 ∈ ℝ ) |
31 |
|
1red |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → 1 ∈ ℝ ) |
32 |
|
elnnuz |
⊢ ( 𝑘 ∈ ℕ ↔ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) |
33 |
|
nnnn0 |
⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 ) |
34 |
32 33
|
sylbir |
⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) → 𝑘 ∈ ℕ0 ) |
35 |
34 18
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → 𝑘 ∈ ℝ ) |
36 |
34 21
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ∈ ℝ ) |
37 |
20
|
absge0d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 0 ≤ ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) |
38 |
34 37
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → 0 ≤ ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) |
39 |
|
eluzle |
⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 1 ) → 1 ≤ 𝑘 ) |
40 |
39
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → 1 ≤ 𝑘 ) |
41 |
31 35 36 38 40
|
lemul1ad |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( 1 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ≤ ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ) |
42 |
|
absidm |
⊢ ( ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ∈ ℂ → ( abs ‘ ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) |
43 |
20 42
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) |
44 |
25
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ‘ 𝑘 ) ) = ( abs ‘ ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ) |
45 |
26
|
mulid2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) |
46 |
43 44 45
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ‘ 𝑘 ) ) = ( 1 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ) |
47 |
34 46
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( abs ‘ ( ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ‘ 𝑘 ) ) = ( 1 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ) |
48 |
16
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 · ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ) = ( 1 · ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ) ) |
49 |
22
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ∈ ℂ ) |
50 |
49
|
mulid2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 · ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ) = ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ) |
51 |
48 50
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 · ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ) = ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ) |
52 |
34 51
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( 1 · ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ) = ( 𝑘 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑘 ) ) ) ) |
53 |
41 47 52
|
3brtr4d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 1 ) ) → ( abs ‘ ( ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ‘ 𝑘 ) ) ≤ ( 1 · ( ( 𝑚 ∈ ℕ0 ↦ ( 𝑚 · ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) ‘ 𝑚 ) ) ) ) ‘ 𝑘 ) ) ) |
54 |
7 9 23 27 29 30 53
|
cvgcmpce |
⊢ ( 𝜑 → seq 0 ( + , ( abs ∘ ( 𝐺 ‘ 𝑋 ) ) ) ∈ dom ⇝ ) |