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

Theorem rpxr 11299
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 11298 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21rexrd 9677 1  |-  ( A  e.  RR+  ->  A  e. 
RR* )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1891   RR*cxr 9661   RR+crp 11292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-rab 2746  df-v 3015  df-un 3377  df-in 3379  df-ss 3386  df-xr 9666  df-rp 11293
This theorem is referenced by:  xlemul1  11566  xlemul2  11567  xltmul1  11568  xltmul2  11569  muladdmodid  12131  sgnrrp  13165  blcntrps  21438  blcntr  21439  unirnblps  21445  unirnbl  21446  blssexps  21452  blssex  21453  blin2  21455  neibl  21527  blnei  21528  metss  21534  metss2lem  21537  stdbdmet  21542  stdbdmopn  21544  mopnex  21545  metrest  21550  prdsxmslem2  21555  metcnp3  21566  metcnp  21567  metcnpi3  21572  txmetcnp  21573  metustid  21580  cfilucfil  21585  blval2  21588  elbl4  21589  metucn  21597  dscopn  21599  nmoix  21745  nmoixOLD  21761  xrsmopn  21841  zdis  21845  reperflem  21847  reconnlem2  21856  metdseq0  21882  metdseq0OLD  21897  cnllycmp  21995  lebnum  22006  xlebnum  22007  lebnumii  22008  nmhmcn  22145  lmmbr  22239  lmmbr2  22240  lmnn  22244  cfilfcls  22255  iscau2  22258  iscmet3lem2  22273  equivcfil  22280  flimcfil  22294  cmpcmet  22298  cncmet  22301  bcthlem5  22307  ellimc3  22846  abelthlem2  23399  abelthlem5  23402  abelthlem7  23405  pige3  23484  dvlog2  23610  efopnlem1  23613  efopnlem2  23614  efopn  23615  logtayl  23617  logtayl2  23619  xrlimcnp  23906  efrlim  23907  lgamcvg2  23992  pntlemi  24454  pntlemp  24460  nvelbl  26337  ubthlem1  26524  xdivpnfrp  28410  pnfinf  28507  signsply0  29446  cnllyscon  29974  poimirlem29  31971  heicant  31977  itg2gt0cn  31999  ftc1anc  32027  areacirclem1  32034  areacirc  32039  blssp  32087  sstotbnd2  32108  isbndx  32116  isbnd2  32117  isbnd3  32118  ssbnd  32122  prdstotbnd  32128  prdsbnd2  32129  cntotbnd  32130  ismtybndlem  32140  heibor1  32144  modelico  35667  infleinflem1  37625  limcrecl  37751  islpcn  37761  etransclem18  38174  etransclem46  38202  sge0iunmptlemre  38316
  Copyright terms: Public domain W3C validator