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 ffvelrnda φ 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