Theorem rpxrd 11269

Description: A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
rpred.1	|- ( ph -> A e. RR+ )

Assertion

Ref	Expression
rpxrd	|- ( ph -> A e. RR* )

Proof of Theorem rpxrd

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 |- ( ph -> A e. RR+ )
2	1	rpred 11268	. 2 |- ( ph -> A e. RR )
3	2	rexrd 9655	1 |- ( ph -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 1767   RR*cxr 9639   RR+crp 11232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2826  df-v 3120  df-un 3486  df-in 3488  df-ss 3495  df-xr 9644  df-rp 11233

This theorem is referenced by:  ssblex  20799  metequiv2  20881  metss2lem  20882  methaus  20891  met1stc  20892  met2ndci  20893  metcnp  20912  metcnpi3  20917  metustexhalfOLD  20934  metustexhalf  20935  blval2  20946  metuel2  20950  nmoi2  21105  metdcnlem  21209  metdscnlem  21227  metnrmlem2  21232  metnrmlem3  21233  cnheibor  21323  cnllycmp  21324  lebnumlem3  21331  nmoleub2lem  21465  nmhmcn  21471  iscfil2  21573  cfil3i  21576  iscfil3  21580  iscmet3lem2  21599  caubl  21614  caublcls  21615  relcmpcmet  21623  bcthlem2  21632  bcthlem4  21634  bcthlem5  21635  ellimc3  22151  ftc1a  22306  ulmdvlem1  22662  psercnlem2  22686  psercn  22688  pserdvlem2  22690  pserdv  22691  efopn  22905  logccv  22910  efrlim  23165  ftalem3  23214  logexprlim  23366  pntpbnd1a  23636  pntleme  23659  pntlem3  23660  pntleml  23662  ubthlem1  25609  ubthlem2  25610  tpr2rico  27719  xrmulc1cn  27737  lgamucov  28405  heicant  29976  ftc1anclem6  30022  ftc1anclem7  30023  sstotbnd2  30197  equivtotbnd  30201  totbndbnd  30212  cntotbnd  30219  heibor1lem  30232  heiborlem3  30236  heiborlem6  30239  heiborlem8  30241  stoweid  31686