Theorem rpxrd 11016

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 11015	. 2 |- ( ph -> A e. RR )
3	2	rexrd 9421	1 |- ( ph -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 1755   RR*cxr 9405   RR+crp 10979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-un 3321  df-in 3323  df-ss 3330  df-xr 9410  df-rp 10980

This theorem is referenced by:  ssblex  19845  metequiv2  19927  metss2lem  19928  methaus  19937  met1stc  19938  met2ndci  19939  metcnp  19958  metcnpi3  19963  metustexhalfOLD  19980  metustexhalf  19981  blval2  19992  metuel2  19996  nmoi2  20151  metdcnlem  20255  metdscnlem  20273  metnrmlem2  20278  metnrmlem3  20279  cnheibor  20369  cnllycmp  20370  lebnumlem3  20377  nmoleub2lem  20511  nmhmcn  20517  iscfil2  20619  cfil3i  20622  iscfil3  20626  iscmet3lem2  20645  caubl  20660  caublcls  20661  relcmpcmet  20669  bcthlem2  20678  bcthlem4  20680  bcthlem5  20681  ellimc3  21196  ftc1a  21351  ulmdvlem1  21750  psercnlem2  21774  psercn  21776  pserdvlem2  21778  pserdv  21779  efopn  21988  logccv  21993  efrlim  22248  ftalem3  22297  logexprlim  22449  pntpbnd1a  22719  pntleme  22742  pntlem3  22743  pntleml  22745  ubthlem1  24094  ubthlem2  24095  tpr2rico  26196  xrmulc1cn  26214  lgamucov  26872  heicant  28270  ftc1anclem6  28316  ftc1anclem7  28317  sstotbnd2  28517  equivtotbnd  28521  totbndbnd  28532  cntotbnd  28539  heibor1lem  28552  heiborlem3  28556  heiborlem6  28559  heiborlem8  28561  stoweid  29704