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 ⊢ G = x ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ x n
radcnv.a ⊢ φ → A : ℕ 0 ⟶ ℂ
psergf.x ⊢ φ → X ∈ ℂ
radcnvlem2.y ⊢ φ → Y ∈ ℂ
radcnvlem2.a ⊢ φ → X < Y
radcnvlem2.c ⊢ φ → seq 0 + G ⁡ Y ∈ dom ⁡ ⇝
Assertion radcnvlem2 ⊢ φ → seq 0 + abs ∘ G ⁡ X ∈ dom ⁡ ⇝

Proof

Step Hyp Ref Expression
1 pser.g ⊢ G = x ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ x n
2 radcnv.a ⊢ φ → A : ℕ 0 ⟶ ℂ
3 psergf.x ⊢ φ → X ∈ ℂ
4 radcnvlem2.y ⊢ φ → Y ∈ ℂ
5 radcnvlem2.a ⊢ φ → X < Y
6 radcnvlem2.c ⊢ φ → seq 0 + G ⁡ Y ∈ dom ⁡ ⇝
7 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
8 1nn0 ⊢ 1 ∈ ℕ 0
9 8 a1i ⊢ φ → 1 ∈ ℕ 0
10 id ⊢ m = k → m = k
11 2fveq3 ⊢ m = k → G ⁡ X ⁡ m = G ⁡ X ⁡ k
12 10 11 oveq12d ⊢ m = k → m ⁢ G ⁡ X ⁡ m = k ⁢ G ⁡ X ⁡ k
13 eqid ⊢ m ∈ ℕ 0 ⟼ m ⁢ G ⁡ X ⁡ m = m ∈ ℕ 0 ⟼ m ⁢ G ⁡ X ⁡ m
14 ovex ⊢ k ⁢ G ⁡ X ⁡ k ∈ V
15 12 13 14 fvmpt ⊢ k ∈ ℕ 0 → m ∈ ℕ 0 ⟼ m ⁢ G ⁡ X ⁡ m ⁡ k = k ⁢ G ⁡ X ⁡ k
16 15 adantl ⊢ φ ∧ k ∈ ℕ 0 → m ∈ ℕ 0 ⟼ m ⁢ G ⁡ X ⁡ m ⁡ k = k ⁢ G ⁡ X ⁡ k
17 nn0re ⊢ k ∈ ℕ 0 → k ∈ ℝ
18 17 adantl ⊢ φ ∧ k ∈ ℕ 0 → k ∈ ℝ
19 1 2 3 psergf ⊢ φ → G ⁡ X : ℕ 0 ⟶ ℂ
20 19 ffvelcdmda ⊢ φ ∧ k ∈ ℕ 0 → G ⁡ X ⁡ k ∈ ℂ
21 20 abscld ⊢ φ ∧ k ∈ ℕ 0 → G ⁡ X ⁡ k ∈ ℝ
22 18 21 remulcld ⊢ φ ∧ k ∈ ℕ 0 → k ⁢ G ⁡ X ⁡ k ∈ ℝ
23 16 22 eqeltrd ⊢ φ ∧ k ∈ ℕ 0 → m ∈ ℕ 0 ⟼ m ⁢ G ⁡ X ⁡ m ⁡ k ∈ ℝ
24 fvco3 ⊢ G ⁡ X : ℕ 0 ⟶ ℂ ∧ k ∈ ℕ 0 → abs ∘ G ⁡ X ⁡ k = G ⁡ X ⁡ k
25 19 24 sylan ⊢ φ ∧ k ∈ ℕ 0 → abs ∘ G ⁡ X ⁡ k = G ⁡ X ⁡ k
26 21 recnd ⊢ φ ∧ k ∈ ℕ 0 → G ⁡ X ⁡ k ∈ ℂ
27 25 26 eqeltrd ⊢ φ ∧ k ∈ ℕ 0 → abs ∘ G ⁡ X ⁡ k ∈ ℂ
28 12 cbvmptv ⊢ m ∈ ℕ 0 ⟼ m ⁢ G ⁡ X ⁡ m = k ∈ ℕ 0 ⟼ k ⁢ G ⁡ X ⁡ k
29 1 2 3 4 5 6 28 radcnvlem1 ⊢ φ → seq 0 + m ∈ ℕ 0 ⟼ m ⁢ G ⁡ X ⁡ m ∈ dom ⁡ ⇝
30 1red ⊢ φ → 1 ∈ ℝ
31 1red ⊢ φ ∧ k ∈ ℤ ≥ 1 → 1 ∈ ℝ
32 elnnuz ⊢ k ∈ ℕ ↔ k ∈ ℤ ≥ 1
33 nnnn0 ⊢ k ∈ ℕ → k ∈ ℕ 0
34 32 33 sylbir ⊢ k ∈ ℤ ≥ 1 → k ∈ ℕ 0
35 34 18 sylan2 ⊢ φ ∧ k ∈ ℤ ≥ 1 → k ∈ ℝ
36 34 21 sylan2 ⊢ φ ∧ k ∈ ℤ ≥ 1 → G ⁡ X ⁡ k ∈ ℝ
37 20 absge0d ⊢ φ ∧ k ∈ ℕ 0 → 0 ≤ G ⁡ X ⁡ k
38 34 37 sylan2 ⊢ φ ∧ k ∈ ℤ ≥ 1 → 0 ≤ G ⁡ X ⁡ k
39 eluzle ⊢ k ∈ ℤ ≥ 1 → 1 ≤ k
40 39 adantl ⊢ φ ∧ k ∈ ℤ ≥ 1 → 1 ≤ k
41 31 35 36 38 40 lemul1ad ⊢ φ ∧ k ∈ ℤ ≥ 1 → 1 ⁢ G ⁡ X ⁡ k ≤ k ⁢ G ⁡ X ⁡ k
42 absidm ⊢ G ⁡ X ⁡ k ∈ ℂ → G ⁡ X ⁡ k = G ⁡ X ⁡ k
43 20 42 syl ⊢ φ ∧ k ∈ ℕ 0 → G ⁡ X ⁡ k = G ⁡ X ⁡ k
44 25 fveq2d ⊢ φ ∧ k ∈ ℕ 0 → abs ∘ G ⁡ X ⁡ k = G ⁡ X ⁡ k
45 26 mullidd ⊢ φ ∧ k ∈ ℕ 0 → 1 ⁢ G ⁡ X ⁡ k = G ⁡ X ⁡ k
46 43 44 45 3eqtr4d ⊢ φ ∧ k ∈ ℕ 0 → abs ∘ G ⁡ X ⁡ k = 1 ⁢ G ⁡ X ⁡ k
47 34 46 sylan2 ⊢ φ ∧ k ∈ ℤ ≥ 1 → abs ∘ G ⁡ X ⁡ k = 1 ⁢ G ⁡ X ⁡ k
48 16 oveq2d ⊢ φ ∧ k ∈ ℕ 0 → 1 ⁢ m ∈ ℕ 0 ⟼ m ⁢ G ⁡ X ⁡ m ⁡ k = 1 ⁢ k ⁢ G ⁡ X ⁡ k
49 22 recnd ⊢ φ ∧ k ∈ ℕ 0 → k ⁢ G ⁡ X ⁡ k ∈ ℂ
50 49 mullidd ⊢ φ ∧ k ∈ ℕ 0 → 1 ⁢ k ⁢ G ⁡ X ⁡ k = k ⁢ G ⁡ X ⁡ k
51 48 50 eqtrd ⊢ φ ∧ k ∈ ℕ 0 → 1 ⁢ m ∈ ℕ 0 ⟼ m ⁢ G ⁡ X ⁡ m ⁡ k = k ⁢ G ⁡ X ⁡ k
52 34 51 sylan2 ⊢ φ ∧ k ∈ ℤ ≥ 1 → 1 ⁢ m ∈ ℕ 0 ⟼ m ⁢ G ⁡ X ⁡ m ⁡ k = k ⁢ G ⁡ X ⁡ k
53 41 47 52 3brtr4d ⊢ φ ∧ k ∈ ℤ ≥ 1 → abs ∘ G ⁡ X ⁡ k ≤ 1 ⁢ m ∈ ℕ 0 ⟼ m ⁢ G ⁡ X ⁡ m ⁡ k
54 7 9 23 27 29 30 53 cvgcmpce ⊢ φ → seq 0 + abs ∘ G ⁡ X ∈ dom ⁡ ⇝