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=\left(x\in ℂ⟼\left(n\in {\mathbb{N}}_0⟼A\left(n\right)x^n\right)\right)$$
	radcnv.a	$$⊢\phi \to A:{\mathbb{N}}_0⟶ℂ$$
	psergf.x	$$⊢\phi \to X\in ℂ$$
	radcnvlem2.y	$$⊢\phi \to Y\in ℂ$$
	radcnvlem2.a	$$⊢\phi \to \left|X\right|<\left|Y\right|$$
	radcnvlem2.c	$$⊢\phi \to seq0\left(+,G\left(Y\right)\right)\in \mathrm{dom}⇝$$
Assertion	radcnvlem3	$$⊢\phi \to seq0\left(+,G\left(X\right)\right)\in \mathrm{dom}⇝$$

Proof

Step	Hyp	Ref	Expression
1		pser.g	$$⊢G=\left(x\in ℂ⟼\left(n\in {\mathbb{N}}_0⟼A\left(n\right)x^n\right)\right)$$
2		radcnv.a	$$⊢\phi \to A:{\mathbb{N}}_0⟶ℂ$$
3		psergf.x	$$⊢\phi \to X\in ℂ$$
4		radcnvlem2.y	$$⊢\phi \to Y\in ℂ$$
5		radcnvlem2.a	$$⊢\phi \to \left|X\right|<\left|Y\right|$$
6		radcnvlem2.c	$$⊢\phi \to seq0\left(+,G\left(Y\right)\right)\in \mathrm{dom}⇝$$
7		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
8		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
9	1 2 3	psergf	$$⊢\phi \to G\left(X\right):{\mathbb{N}}_0⟶ℂ$$
10		fvco3	$$⊢\left(G\left(X\right):{\mathbb{N}}_0⟶ℂ\wedge k\in {\mathbb{N}}_0\right)\to \left(\mathrm{abs}\circ G\left(X\right)\right)\left(k\right)=\left|G\left(X\right)\left(k\right)\right|$$
11	9 10	sylan	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(\mathrm{abs}\circ G\left(X\right)\right)\left(k\right)=\left|G\left(X\right)\left(k\right)\right|$$
12	9	ffvelcdmda	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to G\left(X\right)\left(k\right)\in ℂ$$
13	1 2 3 4 5 6	radcnvlem2	$$⊢\phi \to seq0\left(+,\left(\mathrm{abs}\circ G\left(X\right)\right)\right)\in \mathrm{dom}⇝$$
14	7 8 11 12 13	abscvgcvg	$$⊢\phi \to seq0\left(+,G\left(X\right)\right)\in \mathrm{dom}⇝$$