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

Theorem rpxrd 10651
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 10650 . 2  |-  ( ph  ->  A  e.  RR )
32rexrd 9136 1  |-  ( ph  ->  A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   RR*cxr 9121   RR+crp 10614
This theorem is referenced by:  ssblex  18460  metequiv2  18542  metss2lem  18543  methaus  18552  met1stc  18553  met2ndci  18554  metcnp  18573  metcnpi3  18578  metustexhalfOLD  18595  metustexhalf  18596  blval2  18607  metuel2  18611  nmoi2  18766  metdcnlem  18869  metdscnlem  18887  metnrmlem2  18892  metnrmlem3  18893  cnheibor  18982  cnllycmp  18983  lebnumlem3  18990  nmoleub2lem  19124  nmhmcn  19130  iscfil2  19221  cfil3i  19224  iscfil3  19228  iscmet3lem2  19247  caubl  19262  caublcls  19263  relcmpcmet  19271  bcthlem2  19280  bcthlem4  19282  bcthlem5  19283  ellimc3  19768  ftc1a  19923  ulmdvlem1  20318  psercnlem2  20342  psercn  20344  pserdvlem2  20346  pserdv  20347  efopn  20551  logccv  20556  efrlim  20810  ftalem3  20859  logexprlim  21011  pntpbnd1a  21281  pntleme  21304  pntlem3  21305  pntleml  21307  ubthlem1  22374  ubthlem2  22375  tpr2rico  24312  xrmulc1cn  24318  lgamucov  24824  ftc1anclem6  26287  ftc1anclem7  26288  sstotbnd2  26485  equivtotbnd  26489  totbndbnd  26500  cntotbnd  26507  heibor1lem  26520  heiborlem3  26524  heiborlem6  26527  heiborlem8  26529  stoweid  27790
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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 9126  df-rp 10615
  Copyright terms: Public domain W3C validator