radcnvcl

Description: The radius of convergence R of an infinite series is a nonnegative extended real number. (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* , < )
Assertion	radcnvcl	\|- ( ph -> R e. ( 0 [,] +oo ) )

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		ssrab2	\|- { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR
5		ressxr	\|- RR C_ RR*
6	4 5	sstri	\|- { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR*
7		supxrcl	\|- ( { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR* -> sup ( { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) e. RR* )
8	6 7	mp1i	\|- ( ph -> sup ( { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) e. RR* )
9	3 8	eqeltrid	\|- ( ph -> R e. RR* )
10	1 2	radcnv0	\|- ( ph -> 0 e. { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } )
11		supxrub	\|- ( ( { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } C_ RR* /\ 0 e. { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } ) -> 0 <_ sup ( { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) )
12	6 10 11	sylancr	\|- ( ph -> 0 <_ sup ( { r e. RR \| seq 0 ( + , ( G ` r ) ) e. dom ~~> } , RR* , < ) )
13	12 3	breqtrrdi	\|- ( ph -> 0 <_ R )
14		pnfge	\|- ( R e. RR* -> R <_ +oo )
15	9 14	syl	\|- ( ph -> R <_ +oo )
16		0xr	\|- 0 e. RR*
17		pnfxr	\|- +oo e. RR*
18		elicc1	\|- ( ( 0 e. RR* /\ +oo e. RR* ) -> ( R e. ( 0 [,] +oo ) <-> ( R e. RR* /\ 0 <_ R /\ R <_ +oo ) ) )
19	16 17 18	mp2an	\|- ( R e. ( 0 [,] +oo ) <-> ( R e. RR* /\ 0 <_ R /\ R <_ +oo ) )
20	9 13 15 19	syl3anbrc	\|- ( ph -> R e. ( 0 [,] +oo ) )

Metamath Proof Explorer

Theorem radcnvcl

Proof