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

Theorem rpxr 10994
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 10993 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21rexrd 9429 1  |-  ( A  e.  RR+  ->  A  e. 
RR* )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761   RR*cxr 9413   RR+crp 10987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-un 3330  df-in 3332  df-ss 3339  df-xr 9418  df-rp 10988
This theorem is referenced by:  xlemul1  11249  xlemul2  11250  xltmul1  11251  xltmul2  11252  sgnrrp  12576  blcntrps  19887  blcntr  19888  unirnblps  19894  unirnbl  19895  blssexps  19901  blssex  19902  blin2  19904  neibl  19976  blnei  19977  metss  19983  metss2lem  19986  stdbdmet  19991  stdbdmopn  19993  mopnex  19994  metrest  19999  prdsxmslem2  20004  metcnp3  20015  metcnp  20016  metcnpi3  20021  txmetcnp  20022  metustidOLD  20034  metustid  20035  cfilucfilOLD  20044  cfilucfil  20045  blval2  20050  elbl4  20051  metucnOLD  20063  metucn  20064  dscopn  20066  nmoix  20208  xrsmopn  20289  zdis  20293  reperflem  20295  reconnlem2  20304  metdseq0  20330  cnllycmp  20428  lebnum  20436  xlebnum  20437  lebnumii  20438  nmhmcn  20575  lmmbr  20669  lmmbr2  20670  lmnn  20674  cfilfcls  20685  iscau2  20688  iscmet3lem2  20703  equivcfil  20710  flimcfil  20724  cmpcmet  20728  cncmet  20733  bcthlem5  20739  ellimc3  21254  abelthlem2  21840  abelthlem5  21843  abelthlem7  21846  pige3  21922  dvlog2  22041  efopnlem1  22044  efopnlem2  22045  efopn  22046  logtayl  22048  logtayl2  22050  xrlimcnp  22305  efrlim  22306  pntlemi  22796  pntlemp  22802  nvelbl  24003  ubthlem1  24190  xdivpnfrp  26025  pnfinf  26117  signsply0  26866  lgamcvg2  26955  cnllyscon  27048  heicant  28335  itg2gt0cn  28356  ftc1anc  28384  areacirclem1  28393  areacirc  28398  blssp  28561  sstotbnd2  28582  isbndx  28590  isbnd2  28591  isbnd3  28592  ssbnd  28596  prdstotbnd  28602  prdsbnd2  28603  cntotbnd  28604  ismtybndlem  28614  heibor1  28618  modelico  29071
  Copyright terms: Public domain W3C validator