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

Theorem rpxr 11146
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 11145 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21rexrd 9554 1  |-  ( A  e.  RR+  ->  A  e. 
RR* )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1826   RR*cxr 9538   RR+crp 11139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rab 2741  df-v 3036  df-un 3394  df-in 3396  df-ss 3403  df-xr 9543  df-rp 11140
This theorem is referenced by:  xlemul1  11403  xlemul2  11404  xltmul1  11405  xltmul2  11406  muladdmodid  11937  sgnrrp  12926  blcntrps  21000  blcntr  21001  unirnblps  21007  unirnbl  21008  blssexps  21014  blssex  21015  blin2  21017  neibl  21089  blnei  21090  metss  21096  metss2lem  21099  stdbdmet  21104  stdbdmopn  21106  mopnex  21107  metrest  21112  prdsxmslem2  21117  metcnp3  21128  metcnp  21129  metcnpi3  21134  txmetcnp  21135  metustidOLD  21147  metustid  21148  cfilucfilOLD  21157  cfilucfil  21158  blval2  21163  elbl4  21164  metucnOLD  21176  metucn  21177  dscopn  21179  nmoix  21321  xrsmopn  21402  zdis  21406  reperflem  21408  reconnlem2  21417  metdseq0  21443  cnllycmp  21541  lebnum  21549  xlebnum  21550  lebnumii  21551  nmhmcn  21688  lmmbr  21782  lmmbr2  21783  lmnn  21787  cfilfcls  21798  iscau2  21801  iscmet3lem2  21816  equivcfil  21823  flimcfil  21837  cmpcmet  21841  cncmet  21846  bcthlem5  21852  ellimc3  22368  abelthlem2  22912  abelthlem5  22915  abelthlem7  22918  pige3  22995  dvlog2  23121  efopnlem1  23124  efopnlem2  23125  efopn  23126  logtayl  23128  logtayl2  23130  xrlimcnp  23415  efrlim  23416  pntlemi  23906  pntlemp  23912  nvelbl  25716  ubthlem1  25903  xdivpnfrp  27782  pnfinf  27880  signsply0  28691  lgamcvg2  28786  cnllyscon  28879  heicant  30214  itg2gt0cn  30236  ftc1anc  30264  areacirclem1  30273  areacirc  30278  blssp  30415  sstotbnd2  30436  isbndx  30444  isbnd2  30445  isbnd3  30446  ssbnd  30450  prdstotbnd  30456  prdsbnd2  30457  cntotbnd  30458  ismtybndlem  30468  heibor1  30472  modelico  30922  limcrecl  31801  islpcn  31811  etransclem18  32201  etransclem46  32229
  Copyright terms: Public domain W3C validator