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

Theorem rpxr 11316
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 11315 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21rexrd 9697 1  |-  ( A  e.  RR+  ->  A  e. 
RR* )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872   RR*cxr 9681   RR+crp 11309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780  df-v 3082  df-un 3441  df-in 3443  df-ss 3450  df-xr 9686  df-rp 11310
This theorem is referenced by:  xlemul1  11583  xlemul2  11584  xltmul1  11585  xltmul2  11586  muladdmodid  12143  sgnrrp  13154  blcntrps  21425  blcntr  21426  unirnblps  21432  unirnbl  21433  blssexps  21439  blssex  21440  blin2  21442  neibl  21514  blnei  21515  metss  21521  metss2lem  21524  stdbdmet  21529  stdbdmopn  21531  mopnex  21532  metrest  21537  prdsxmslem2  21542  metcnp3  21553  metcnp  21554  metcnpi3  21559  txmetcnp  21560  metustid  21567  cfilucfil  21572  blval2  21575  elbl4  21576  metucn  21584  dscopn  21586  nmoix  21732  nmoixOLD  21748  xrsmopn  21828  zdis  21832  reperflem  21834  reconnlem2  21843  metdseq0  21869  metdseq0OLD  21884  cnllycmp  21982  lebnum  21993  xlebnum  21994  lebnumii  21995  nmhmcn  22132  lmmbr  22226  lmmbr2  22227  lmnn  22231  cfilfcls  22242  iscau2  22245  iscmet3lem2  22260  equivcfil  22267  flimcfil  22281  cmpcmet  22285  cncmet  22288  bcthlem5  22294  ellimc3  22832  abelthlem2  23385  abelthlem5  23388  abelthlem7  23391  pige3  23470  dvlog2  23596  efopnlem1  23599  efopnlem2  23600  efopn  23601  logtayl  23603  logtayl2  23605  xrlimcnp  23892  efrlim  23893  lgamcvg2  23978  pntlemi  24440  pntlemp  24446  nvelbl  26323  ubthlem1  26510  xdivpnfrp  28409  pnfinf  28507  signsply0  29448  cnllyscon  29976  poimirlem29  31933  heicant  31939  itg2gt0cn  31961  ftc1anc  31989  areacirclem1  31996  areacirc  32001  blssp  32049  sstotbnd2  32070  isbndx  32078  isbnd2  32079  isbnd3  32080  ssbnd  32084  prdstotbnd  32090  prdsbnd2  32091  cntotbnd  32092  ismtybndlem  32102  heibor1  32106  modelico  35635  limcrecl  37649  islpcn  37659  etransclem18  38057  etransclem46  38085  sge0iunmptlemre  38165
  Copyright terms: Public domain W3C validator