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