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

Theorem rpxrd 10654
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 10653 . 2  |-  ( ph  ->  A  e.  RR )
32rexrd 9139 1  |-  ( ph  ->  A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   RR*cxr 9124   RR+crp 10617
This theorem is referenced by:  ssblex  18463  metequiv2  18545  metss2lem  18546  methaus  18555  met1stc  18556  met2ndci  18557  metcnp  18576  metcnpi3  18581  metustexhalfOLD  18598  metustexhalf  18599  blval2  18610  metuel2  18614  nmoi2  18769  metdcnlem  18872  metdscnlem  18890  metnrmlem2  18895  metnrmlem3  18896  cnheibor  18985  cnllycmp  18986  lebnumlem3  18993  nmoleub2lem  19127  nmhmcn  19133  iscfil2  19224  cfil3i  19227  iscfil3  19231  iscmet3lem2  19250  caubl  19265  caublcls  19266  relcmpcmet  19274  bcthlem2  19283  bcthlem4  19285  bcthlem5  19286  ellimc3  19771  ftc1a  19926  ulmdvlem1  20321  psercnlem2  20345  psercn  20347  pserdvlem2  20349  pserdv  20350  efopn  20554  logccv  20559  efrlim  20813  ftalem3  20862  logexprlim  21014  pntpbnd1a  21284  pntleme  21307  pntlem3  21308  pntleml  21310  ubthlem1  22377  ubthlem2  22378  tpr2rico  24315  xrmulc1cn  24321  lgamucov  24827  heicant  26253  ftc1anclem6  26299  ftc1anclem7  26300  sstotbnd2  26497  equivtotbnd  26501  totbndbnd  26512  cntotbnd  26519  heibor1lem  26532  heiborlem3  26536  heiborlem6  26539  heiborlem8  26541  stoweid  27802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-un 3327  df-in 3329  df-ss 3336  df-xr 9129  df-rp 10618
  Copyright terms: Public domain W3C validator