Metamath Proof Explorer


Theorem 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 n 0 A n x n
radcnv.a φ A : 0
radcnv.r R = sup r | seq 0 + G r dom * <
Assertion radcnvcl φ R 0 +∞

Proof

Step Hyp Ref Expression
1 pser.g G = x n 0 A n x n
2 radcnv.a φ A : 0
3 radcnv.r R = sup r | seq 0 + G r dom * <
4 ssrab2 r | seq 0 + G r dom
5 ressxr *
6 4 5 sstri r | seq 0 + G r dom *
7 supxrcl r | seq 0 + G r dom * sup r | seq 0 + G r dom * < *
8 6 7 mp1i φ sup r | seq 0 + G r dom * < *
9 3 8 eqeltrid φ R *
10 1 2 radcnv0 φ 0 r | seq 0 + G r dom
11 supxrub r | seq 0 + G r dom * 0 r | seq 0 + G r dom 0 sup r | seq 0 + G r dom * <
12 6 10 11 sylancr φ 0 sup r | seq 0 + G r dom * <
13 12 3 breqtrrdi φ 0 R
14 pnfge R * R +∞
15 9 14 syl φ R +∞
16 0xr 0 *
17 pnfxr +∞ *
18 elicc1 0 * +∞ * R 0 +∞ R * 0 R R +∞
19 16 17 18 mp2an R 0 +∞ R * 0 R R +∞
20 9 13 15 19 syl3anbrc φ R 0 +∞