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=\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	radcnvlem2	$$⊢\phi \to seq0\left(+,\left(\mathrm{abs}\circ G\left(X\right)\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		1nn0	$$⊢1\in {\mathbb{N}}_0$$
9	8	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
10		id	$$⊢m=k\to m=k$$
11		2fveq3	$$⊢m=k\to \left|G\left(X\right)\left(m\right)\right|=\left|G\left(X\right)\left(k\right)\right|$$
12	10 11	oveq12d	$$⊢m=k\to m\left|G\left(X\right)\left(m\right)\right|=k\left|G\left(X\right)\left(k\right)\right|$$
13		eqid	$$⊢\left(m\in {\mathbb{N}}_0⟼m\left|G\left(X\right)\left(m\right)\right|\right)=\left(m\in {\mathbb{N}}_0⟼m\left|G\left(X\right)\left(m\right)\right|\right)$$
14		ovex	$$⊢k\left|G\left(X\right)\left(k\right)\right|\in \mathrm{V}$$
15	12 13 14	fvmpt	$$⊢k\in {\mathbb{N}}_0\to \left(m\in {\mathbb{N}}_0⟼m\left|G\left(X\right)\left(m\right)\right|\right)\left(k\right)=k\left|G\left(X\right)\left(k\right)\right|$$
16	15	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(m\in {\mathbb{N}}_0⟼m\left|G\left(X\right)\left(m\right)\right|\right)\left(k\right)=k\left|G\left(X\right)\left(k\right)\right|$$
17		nn0re	$$⊢k\in {\mathbb{N}}_0\to k\in ℝ$$
18	17	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k\in ℝ$$
19	1 2 3	psergf	$$⊢\phi \to G\left(X\right):{\mathbb{N}}_0⟶ℂ$$
20	19	ffvelcdmda	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to G\left(X\right)\left(k\right)\in ℂ$$
21	20	abscld	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left|G\left(X\right)\left(k\right)\right|\in ℝ$$
22	18 21	remulcld	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k\left|G\left(X\right)\left(k\right)\right|\in ℝ$$
23	16 22	eqeltrd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(m\in {\mathbb{N}}_0⟼m\left|G\left(X\right)\left(m\right)\right|\right)\left(k\right)\in ℝ$$
24		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|$$
25	19 24	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|$$
26	21	recnd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left|G\left(X\right)\left(k\right)\right|\in ℂ$$
27	25 26	eqeltrd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(\mathrm{abs}\circ G\left(X\right)\right)\left(k\right)\in ℂ$$
28	12	cbvmptv	$$⊢\left(m\in {\mathbb{N}}_0⟼m\left|G\left(X\right)\left(m\right)\right|\right)=\left(k\in {\mathbb{N}}_0⟼k\left|G\left(X\right)\left(k\right)\right|\right)$$
29	1 2 3 4 5 6 28	radcnvlem1	$$⊢\phi \to seq0\left(+,\left(m\in {\mathbb{N}}_0⟼m\left|G\left(X\right)\left(m\right)\right|\right)\right)\in \mathrm{dom}⇝$$
30		1red	$$⊢\phi \to 1\in ℝ$$
31		1red	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to 1\in ℝ$$
32		elnnuz	$$⊢k\in \mathbb{N}\leftrightarrow k\in {\mathbb{Z}}_{\ge 1}$$
33		nnnn0	$$⊢k\in \mathbb{N}\to k\in {\mathbb{N}}_0$$
34	32 33	sylbir	$$⊢k\in {\mathbb{Z}}_{\ge 1}\to k\in {\mathbb{N}}_0$$
35	34 18	sylan2	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to k\in ℝ$$
36	34 21	sylan2	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to \left|G\left(X\right)\left(k\right)\right|\in ℝ$$
37	20	absge0d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to 0\le \left|G\left(X\right)\left(k\right)\right|$$
38	34 37	sylan2	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to 0\le \left|G\left(X\right)\left(k\right)\right|$$
39		eluzle	$$⊢k\in {\mathbb{Z}}_{\ge 1}\to 1\le k$$
40	39	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to 1\le k$$
41	31 35 36 38 40	lemul1ad	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to 1\left|G\left(X\right)\left(k\right)\right|\le k\left|G\left(X\right)\left(k\right)\right|$$
42		absidm	$$⊢G\left(X\right)\left(k\right)\in ℂ\to \left|\left|G\left(X\right)\left(k\right)\right|\right|=\left|G\left(X\right)\left(k\right)\right|$$
43	20 42	syl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left|\left|G\left(X\right)\left(k\right)\right|\right|=\left|G\left(X\right)\left(k\right)\right|$$
44	25	fveq2d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left|\left(\mathrm{abs}\circ G\left(X\right)\right)\left(k\right)\right|=\left|\left|G\left(X\right)\left(k\right)\right|\right|$$
45	26	mullidd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to 1\left|G\left(X\right)\left(k\right)\right|=\left|G\left(X\right)\left(k\right)\right|$$
46	43 44 45	3eqtr4d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left|\left(\mathrm{abs}\circ G\left(X\right)\right)\left(k\right)\right|=1\left|G\left(X\right)\left(k\right)\right|$$
47	34 46	sylan2	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to \left|\left(\mathrm{abs}\circ G\left(X\right)\right)\left(k\right)\right|=1\left|G\left(X\right)\left(k\right)\right|$$
48	16	oveq2d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to 1\left(m\in {\mathbb{N}}_0⟼m\left|G\left(X\right)\left(m\right)\right|\right)\left(k\right)=1k\left|G\left(X\right)\left(k\right)\right|$$
49	22	recnd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k\left|G\left(X\right)\left(k\right)\right|\in ℂ$$
50	49	mullidd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to 1k\left|G\left(X\right)\left(k\right)\right|=k\left|G\left(X\right)\left(k\right)\right|$$
51	48 50	eqtrd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to 1\left(m\in {\mathbb{N}}_0⟼m\left|G\left(X\right)\left(m\right)\right|\right)\left(k\right)=k\left|G\left(X\right)\left(k\right)\right|$$
52	34 51	sylan2	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to 1\left(m\in {\mathbb{N}}_0⟼m\left|G\left(X\right)\left(m\right)\right|\right)\left(k\right)=k\left|G\left(X\right)\left(k\right)\right|$$
53	41 47 52	3brtr4d	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge 1}\right)\to \left|\left(\mathrm{abs}\circ G\left(X\right)\right)\left(k\right)\right|\le 1\left(m\in {\mathbb{N}}_0⟼m\left|G\left(X\right)\left(m\right)\right|\right)\left(k\right)$$
54	7 9 23 27 29 30 53	cvgcmpce	$$⊢\phi \to seq0\left(+,\left(\mathrm{abs}\circ G\left(X\right)\right)\right)\in \mathrm{dom}⇝$$