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

Theorem rpxrd 10407
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 10406 . 2  |-  ( ph  ->  A  e.  RR )
32rexrd 8897 1  |-  ( ph  ->  A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   RR*cxr 8882   RR+crp 10370
This theorem is referenced by:  ssblex  17990  metequiv2  18072  metss2lem  18073  methaus  18082  met1stc  18083  met2ndci  18084  metcnp  18103  metcnpi3  18108  nmoi2  18255  metdcnlem  18357  metdscnlem  18375  metnrmlem2  18380  metnrmlem3  18381  cnheibor  18469  cnllycmp  18470  lebnumlem3  18477  nmoleub2lem  18611  nmhmcn  18617  iscfil2  18708  cfil3i  18711  iscfil3  18715  iscmet3lem2  18734  caubl  18749  caublcls  18750  relcmpcmet  18758  bcthlem2  18763  bcthlem4  18765  bcthlem5  18766  ellimc3  19245  ftc1a  19400  ulmdvlem1  19793  psercnlem2  19816  psercn  19818  pserdvlem2  19820  pserdv  19821  efopn  20021  logccv  20026  efrlim  20280  ftalem3  20328  logexprlim  20480  pntpbnd1a  20750  pntleme  20773  pntlem3  20774  pntleml  20776  ubthlem1  21465  ubthlem2  21466  tpr2rico  23311  xrmulc1cn  23318  sstotbnd2  26601  totbndbnd  26616  heibor1lem  26636  heiborlem3  26640  heiborlem6  26643  heiborlem8  26645
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-un 3170  df-in 3172  df-ss 3179  df-xr 8887  df-rp 10371
  Copyright terms: Public domain W3C validator