radcnvle

Description: If X is a convergent point of the infinite series, then X is within the closed disk of radius R centered at zero. Or, by contraposition, the series diverges at any point strictly more than R from the origin. (Contributed by Mario Carneiro, 26-Feb-2015)

	Ref	Expression
Hypotheses	pser.g	\|- G = ( x e. CC \|-> ( n e. NN0 \|-> ( ( A ` n ) x. ( x ^ n ) ) ) )
	radcnv.a	\|- ( ph -> A : NN0 --> CC )
	radcnv.r	\|- R = sup ( { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
	radcnvle.x	\|- ( ph -> X e. CC )
	radcnvle.a	\|- ( ph -> seq 0 ( + , ( G ` X ) ) e. dom ~~> )
Assertion	radcnvle	\|- ( ph -> ( abs ` X ) <_ R )

Proof

Step	Hyp	Ref	Expression
1		pser.g	\|- G = ( x e. CC \|-> ( n e. NN0 \|-> ( ( A ` n ) x. ( x ^ n ) ) ) )
2		radcnv.a	\|- ( ph -> A : NN0 --> CC )
3		radcnv.r	\|- R = sup ( { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < )
4		radcnvle.x	\|- ( ph -> X e. CC )
5		radcnvle.a	\|- ( ph -> seq 0 ( + , ( G ` X ) ) e. dom ~~> )
6		ressxr	\|- RR C_ RR*
7	4	abscld	\|- ( ph -> ( abs ` X ) e. RR )
8	6 7	sselid	\|- ( ph -> ( abs ` X ) e. RR* )
9		iccssxr	\|- ( 0 [,] +oo ) C_ RR*
10	1 2 3	radcnvcl	\|- ( ph -> R e. ( 0 [,] +oo ) )
11	9 10	sselid	\|- ( ph -> R e. RR* )
12		simpr	\|- ( ( ph /\ R < ( abs ` X ) ) -> R < ( abs ` X ) )
13	11	adantr	\|- ( ( ph /\ R < ( abs ` X ) ) -> R e. RR* )
14	7	adantr	\|- ( ( ph /\ R < ( abs ` X ) ) -> ( abs ` X ) e. RR )
15		0xr	\|- 0 e. RR*
16		pnfxr	\|- +oo e. RR*
17		elicc1	\|- ( ( 0 e. RR* /\ +oo e. RR* ) -> ( R e. ( 0 [,] +oo ) <-> ( R e. RR* /\ 0 <_ R /\ R <_ +oo ) ) )
18	15 16 17	mp2an	\|- ( R e. ( 0 [,] +oo ) <-> ( R e. RR* /\ 0 <_ R /\ R <_ +oo ) )
19	10 18	sylib	\|- ( ph -> ( R e. RR* /\ 0 <_ R /\ R <_ +oo ) )
20	19	simp2d	\|- ( ph -> 0 <_ R )
21		ge0gtmnf	\|- ( ( R e. RR* /\ 0 <_ R ) -> -oo < R )
22	11 20 21	syl2anc	\|- ( ph -> -oo < R )
23	22	adantr	\|- ( ( ph /\ R < ( abs ` X ) ) -> -oo < R )
24	8	adantr	\|- ( ( ph /\ R < ( abs ` X ) ) -> ( abs ` X ) e. RR* )
25	13 24 12	xrltled	\|- ( ( ph /\ R < ( abs ` X ) ) -> R <_ ( abs ` X ) )
26		xrre	\|- ( ( ( R e. RR* /\ ( abs ` X ) e. RR ) /\ ( -oo < R /\ R <_ ( abs ` X ) ) ) -> R e. RR )
27	13 14 23 25 26	syl22anc	\|- ( ( ph /\ R < ( abs ` X ) ) -> R e. RR )
28		avglt1	\|- ( ( R e. RR /\ ( abs ` X ) e. RR ) -> ( R < ( abs ` X ) <-> R < ( ( R + ( abs ` X ) ) / 2 ) ) )
29	27 14 28	syl2anc	\|- ( ( ph /\ R < ( abs ` X ) ) -> ( R < ( abs ` X ) <-> R < ( ( R + ( abs ` X ) ) / 2 ) ) )
30	12 29	mpbid	\|- ( ( ph /\ R < ( abs ` X ) ) -> R < ( ( R + ( abs ` X ) ) / 2 ) )
31	27 14	readdcld	\|- ( ( ph /\ R < ( abs ` X ) ) -> ( R + ( abs ` X ) ) e. RR )
32	31	rehalfcld	\|- ( ( ph /\ R < ( abs ` X ) ) -> ( ( R + ( abs ` X ) ) / 2 ) e. RR )
33		ssrab2	\|- { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR
34	33 6	sstri	\|- { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR*
35	2	adantr	\|- ( ( ph /\ R < ( abs ` X ) ) -> A : NN0 --> CC )
36	32	recnd	\|- ( ( ph /\ R < ( abs ` X ) ) -> ( ( R + ( abs ` X ) ) / 2 ) e. CC )
37	4	adantr	\|- ( ( ph /\ R < ( abs ` X ) ) -> X e. CC )
38		0red	\|- ( ( ph /\ R < ( abs ` X ) ) -> 0 e. RR )
39	20	adantr	\|- ( ( ph /\ R < ( abs ` X ) ) -> 0 <_ R )
40	38 27 32 39 30	lelttrd	\|- ( ( ph /\ R < ( abs ` X ) ) -> 0 < ( ( R + ( abs ` X ) ) / 2 ) )
41	38 32 40	ltled	\|- ( ( ph /\ R < ( abs ` X ) ) -> 0 <_ ( ( R + ( abs ` X ) ) / 2 ) )
42	32 41	absidd	\|- ( ( ph /\ R < ( abs ` X ) ) -> ( abs ` ( ( R + ( abs ` X ) ) / 2 ) ) = ( ( R + ( abs ` X ) ) / 2 ) )
43		avglt2	\|- ( ( R e. RR /\ ( abs ` X ) e. RR ) -> ( R < ( abs ` X ) <-> ( ( R + ( abs ` X ) ) / 2 ) < ( abs ` X ) ) )
44	27 14 43	syl2anc	\|- ( ( ph /\ R < ( abs ` X ) ) -> ( R < ( abs ` X ) <-> ( ( R + ( abs ` X ) ) / 2 ) < ( abs ` X ) ) )
45	12 44	mpbid	\|- ( ( ph /\ R < ( abs ` X ) ) -> ( ( R + ( abs ` X ) ) / 2 ) < ( abs ` X ) )
46	42 45	eqbrtrd	\|- ( ( ph /\ R < ( abs ` X ) ) -> ( abs ` ( ( R + ( abs ` X ) ) / 2 ) ) < ( abs ` X ) )
47	5	adantr	\|- ( ( ph /\ R < ( abs ` X ) ) -> seq 0 ( + , ( G ` X ) ) e. dom ~~> )
48	1 35 36 37 46 47	radcnvlem3	\|- ( ( ph /\ R < ( abs ` X ) ) -> seq 0 ( + , ( G ` ( ( R + ( abs ` X ) ) / 2 ) ) ) e. dom ~~> )
49		fveq2	\|- ( y = ( ( R + ( abs ` X ) ) / 2 ) -> ( G ` y ) = ( G ` ( ( R + ( abs ` X ) ) / 2 ) ) )
50	49	seqeq3d	\|- ( y = ( ( R + ( abs ` X ) ) / 2 ) -> seq 0 ( + , ( G ` y ) ) = seq 0 ( + , ( G ` ( ( R + ( abs ` X ) ) / 2 ) ) ) )
51	50	eleq1d	\|- ( y = ( ( R + ( abs ` X ) ) / 2 ) -> ( seq 0 ( + , ( G ` y ) ) e. dom ~~> <-> seq 0 ( + , ( G ` ( ( R + ( abs ` X ) ) / 2 ) ) ) e. dom ~~> ) )
52		fveq2	\|- ( r = y -> ( G ` r ) = ( G ` y ) )
53	52	seqeq3d	\|- ( r = y -> seq 0 ( + , ( G ` r ) ) = seq 0 ( + , ( G ` y ) ) )
54	53	eleq1d	\|- ( r = y -> ( seq 0 ( + , ( G ` r ) ) e. dom ~~> <-> seq 0 ( + , ( G ` y ) ) e. dom ~~> ) )
55	54	cbvrabv	\|- { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } = { y e. RR \| seq 0 ( + , ( G ` y ) ) e. dom ~~> }
56	51 55	elrab2	\|- ( ( ( R + ( abs ` X ) ) / 2 ) e. { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } <-> ( ( ( R + ( abs ` X ) ) / 2 ) e. RR /\ seq 0 ( + , ( G ` ( ( R + ( abs ` X ) ) / 2 ) ) ) e. dom ~~> ) )
57	32 48 56	sylanbrc	\|- ( ( ph /\ R < ( abs ` X ) ) -> ( ( R + ( abs ` X ) ) / 2 ) e. { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } )
58		supxrub	\|- ( ( { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR* /\ ( ( R + ( abs ` X ) ) / 2 ) e. { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) -> ( ( R + ( abs ` X ) ) / 2 ) <_ sup ( { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) )
59	34 57 58	sylancr	\|- ( ( ph /\ R < ( abs ` X ) ) -> ( ( R + ( abs ` X ) ) / 2 ) <_ sup ( { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) )
60	59 3	breqtrrdi	\|- ( ( ph /\ R < ( abs ` X ) ) -> ( ( R + ( abs ` X ) ) / 2 ) <_ R )
61	32 27 60	lensymd	\|- ( ( ph /\ R < ( abs ` X ) ) -> -. R < ( ( R + ( abs ` X ) ) / 2 ) )
62	30 61	pm2.65da	\|- ( ph -> -. R < ( abs ` X ) )
63	8 11 62	xrnltled	\|- ( ph -> ( abs ` X ) <_ R )

Metamath Proof Explorer

Theorem radcnvle

Proof