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

Theorem rpxrd 10542
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 10541 . 2  |-  ( ph  ->  A  e.  RR )
32rexrd 9028 1  |-  ( ph  ->  A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1715   RR*cxr 9013   RR+crp 10505
This theorem is referenced by:  ssblex  18187  metequiv2  18269  metss2lem  18270  methaus  18279  met1stc  18280  met2ndci  18281  metcnp  18300  metcnpi3  18305  nmoi2  18452  metdcnlem  18555  metdscnlem  18573  metnrmlem2  18578  metnrmlem3  18579  cnheibor  18668  cnllycmp  18669  lebnumlem3  18676  nmoleub2lem  18810  nmhmcn  18816  iscfil2  18907  cfil3i  18910  iscfil3  18914  iscmet3lem2  18933  caubl  18948  caublcls  18949  relcmpcmet  18957  bcthlem2  18962  bcthlem4  18964  bcthlem5  18965  ellimc3  19444  ftc1a  19599  ulmdvlem1  19994  psercnlem2  20018  psercn  20020  pserdvlem2  20022  pserdv  20023  efopn  20227  logccv  20232  efrlim  20486  ftalem3  20535  logexprlim  20687  pntpbnd1a  20957  pntleme  20980  pntlem3  20981  pntleml  20983  ubthlem1  21883  ubthlem2  21884  tpr2rico  23786  xrmulc1cn  23792  metustexhalf  23920  blval2  23928  lgamucov  24391  sstotbnd2  26089  totbndbnd  26104  heibor1lem  26124  heiborlem3  26128  heiborlem6  26131  heiborlem8  26133
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rab 2637  df-v 2875  df-un 3243  df-in 3245  df-ss 3252  df-xr 9018  df-rp 10506
  Copyright terms: Public domain W3C validator