This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem radcnvlem3

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 at X . (Contributed by Mario Carneiro, 31-Mar-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 radcnvlem3 ⊢ φ → seq 0 + 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 0zd ⊢ φ → 0 ∈ ℤ
9 1 2 3 psergf ⊢ φ → G ⁡ X : ℕ 0 ⟶ ℂ
10 fvco3 ⊢ G ⁡ X : ℕ 0 ⟶ ℂ ∧ k ∈ ℕ 0 → abs ∘ G ⁡ X ⁡ k = G ⁡ X ⁡ k
11 9 10 sylan ⊢ φ ∧ k ∈ ℕ 0 → abs ∘ G ⁡ X ⁡ k = G ⁡ X ⁡ k
12 9 ffvelcdmda ⊢ φ ∧ k ∈ ℕ 0 → G ⁡ X ⁡ k ∈ ℂ
13 1 2 3 4 5 6 radcnvlem2 ⊢ φ → seq 0 + abs ∘ G ⁡ X ∈ dom ⁡ ⇝
14 7 8 11 12 13 abscvgcvg ⊢ φ → seq 0 + G ⁡ X ∈ dom ⁡ ⇝