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

Theorem rpxr 11227
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 11226 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21rexrd 9643 1  |-  ( A  e.  RR+  ->  A  e. 
RR* )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   RR*cxr 9627   RR+crp 11220
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-un 3481  df-in 3483  df-ss 3490  df-xr 9632  df-rp 11221
This theorem is referenced by:  xlemul1  11482  xlemul2  11483  xltmul1  11484  xltmul2  11485  sgnrrp  12887  blcntrps  20678  blcntr  20679  unirnblps  20685  unirnbl  20686  blssexps  20692  blssex  20693  blin2  20695  neibl  20767  blnei  20768  metss  20774  metss2lem  20777  stdbdmet  20782  stdbdmopn  20784  mopnex  20785  metrest  20790  prdsxmslem2  20795  metcnp3  20806  metcnp  20807  metcnpi3  20812  txmetcnp  20813  metustidOLD  20825  metustid  20826  cfilucfilOLD  20835  cfilucfil  20836  blval2  20841  elbl4  20842  metucnOLD  20854  metucn  20855  dscopn  20857  nmoix  20999  xrsmopn  21080  zdis  21084  reperflem  21086  reconnlem2  21095  metdseq0  21121  cnllycmp  21219  lebnum  21227  xlebnum  21228  lebnumii  21229  nmhmcn  21366  lmmbr  21460  lmmbr2  21461  lmnn  21465  cfilfcls  21476  iscau2  21479  iscmet3lem2  21494  equivcfil  21501  flimcfil  21515  cmpcmet  21519  cncmet  21524  bcthlem5  21530  ellimc3  22046  abelthlem2  22589  abelthlem5  22592  abelthlem7  22595  pige3  22671  dvlog2  22790  efopnlem1  22793  efopnlem2  22794  efopn  22795  logtayl  22797  logtayl2  22799  xrlimcnp  23054  efrlim  23055  pntlemi  23545  pntlemp  23551  nvelbl  25303  ubthlem1  25490  xdivpnfrp  27325  pnfinf  27417  signsply0  28176  lgamcvg2  28265  cnllyscon  28358  heicant  29654  itg2gt0cn  29675  ftc1anc  29703  areacirclem1  29712  areacirc  29717  blssp  29880  sstotbnd2  29901  isbndx  29909  isbnd2  29910  isbnd3  29911  ssbnd  29915  prdstotbnd  29921  prdsbnd2  29922  cntotbnd  29923  ismtybndlem  29933  heibor1  29937  modelico  30389  limcrecl  31199  islpcn  31209
  Copyright terms: Public domain W3C validator