MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rpxrd Unicode version

Theorem rpxrd 10605
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
StepHypRef Expression
1 rpred.1 . . 3  |-  ( ph  ->  A  e.  RR+ )
21rpred 10604 . 2  |-  ( ph  ->  A  e.  RR )
32rexrd 9090 1  |-  ( ph  ->  A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   RR*cxr 9075   RR+crp 10568
This theorem is referenced by:  ssblex  18411  metequiv2  18493  metss2lem  18494  methaus  18503  met1stc  18504  met2ndci  18505  metcnp  18524  metcnpi3  18529  metustexhalfOLD  18546  metustexhalf  18547  blval2  18558  metuel2  18562  nmoi2  18717  metdcnlem  18820  metdscnlem  18838  metnrmlem2  18843  metnrmlem3  18844  cnheibor  18933  cnllycmp  18934  lebnumlem3  18941  nmoleub2lem  19075  nmhmcn  19081  iscfil2  19172  cfil3i  19175  iscfil3  19179  iscmet3lem2  19198  caubl  19213  caublcls  19214  relcmpcmet  19222  bcthlem2  19231  bcthlem4  19233  bcthlem5  19234  ellimc3  19719  ftc1a  19874  ulmdvlem1  20269  psercnlem2  20293  psercn  20295  pserdvlem2  20297  pserdv  20298  efopn  20502  logccv  20507  efrlim  20761  ftalem3  20810  logexprlim  20962  pntpbnd1a  21232  pntleme  21255  pntlem3  21256  pntleml  21258  ubthlem1  22325  ubthlem2  22326  tpr2rico  24263  xrmulc1cn  24269  lgamucov  24775  sstotbnd2  26373  equivtotbnd  26377  totbndbnd  26388  cntotbnd  26395  heibor1lem  26408  heiborlem3  26412  heiborlem6  26415  heiborlem8  26417  stoweid  27679
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-un 3285  df-in 3287  df-ss 3294  df-xr 9080  df-rp 10569
  Copyright terms: Public domain W3C validator