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

Theorem rpxr 10998
Description: A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
rpxr  |-  ( A  e.  RR+  ->  A  e. 
RR* )

Proof of Theorem rpxr
StepHypRef Expression
1 rpre 10997 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21rexrd 9433 1  |-  ( A  e.  RR+  ->  A  e. 
RR* )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   RR*cxr 9417   RR+crp 10991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rab 2724  df-v 2974  df-un 3333  df-in 3335  df-ss 3342  df-xr 9422  df-rp 10992
This theorem is referenced by:  xlemul1  11253  xlemul2  11254  xltmul1  11255  xltmul2  11256  sgnrrp  12580  blcntrps  19987  blcntr  19988  unirnblps  19994  unirnbl  19995  blssexps  20001  blssex  20002  blin2  20004  neibl  20076  blnei  20077  metss  20083  metss2lem  20086  stdbdmet  20091  stdbdmopn  20093  mopnex  20094  metrest  20099  prdsxmslem2  20104  metcnp3  20115  metcnp  20116  metcnpi3  20121  txmetcnp  20122  metustidOLD  20134  metustid  20135  cfilucfilOLD  20144  cfilucfil  20145  blval2  20150  elbl4  20151  metucnOLD  20163  metucn  20164  dscopn  20166  nmoix  20308  xrsmopn  20389  zdis  20393  reperflem  20395  reconnlem2  20404  metdseq0  20430  cnllycmp  20528  lebnum  20536  xlebnum  20537  lebnumii  20538  nmhmcn  20675  lmmbr  20769  lmmbr2  20770  lmnn  20774  cfilfcls  20785  iscau2  20788  iscmet3lem2  20803  equivcfil  20810  flimcfil  20824  cmpcmet  20828  cncmet  20833  bcthlem5  20839  ellimc3  21354  abelthlem2  21897  abelthlem5  21900  abelthlem7  21903  pige3  21979  dvlog2  22098  efopnlem1  22101  efopnlem2  22102  efopn  22103  logtayl  22105  logtayl2  22107  xrlimcnp  22362  efrlim  22363  pntlemi  22853  pntlemp  22859  nvelbl  24084  ubthlem1  24271  xdivpnfrp  26108  pnfinf  26200  signsply0  26952  lgamcvg2  27041  cnllyscon  27134  heicant  28426  itg2gt0cn  28447  ftc1anc  28475  areacirclem1  28484  areacirc  28489  blssp  28652  sstotbnd2  28673  isbndx  28681  isbnd2  28682  isbnd3  28683  ssbnd  28687  prdstotbnd  28693  prdsbnd2  28694  cntotbnd  28695  ismtybndlem  28705  heibor1  28709  modelico  29162
  Copyright terms: Public domain W3C validator