Metamath Proof Explorer


Theorem radcnvlem2

Description: Lemma for radcnvlt1 , radcnvle . If X is a point closer to zero than Y and the power series converges at Y , then it converges absolutely at X . (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Hypotheses pser.g 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) · ( 𝑥𝑛 ) ) ) )
radcnv.a ( 𝜑𝐴 : ℕ0 ⟶ ℂ )
psergf.x ( 𝜑𝑋 ∈ ℂ )
radcnvlem2.y ( 𝜑𝑌 ∈ ℂ )
radcnvlem2.a ( 𝜑 → ( abs ‘ 𝑋 ) < ( abs ‘ 𝑌 ) )
radcnvlem2.c ( 𝜑 → seq 0 ( + , ( 𝐺𝑌 ) ) ∈ dom ⇝ )
Assertion radcnvlem2 ( 𝜑 → seq 0 ( + , ( abs ∘ ( 𝐺𝑋 ) ) ) ∈ dom ⇝ )

Proof

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 ⇝ )