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

Theorem rpxr 10575
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 10574 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21rexrd 9090 1  |-  ( A  e.  RR+  ->  A  e. 
RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   RR*cxr 9075   RR+crp 10568
This theorem is referenced by:  xlemul1  10825  xlemul2  10826  xltmul1  10827  xltmul2  10828  blcntrps  18395  blcntr  18396  unirnblps  18402  unirnbl  18403  blssexps  18409  blssex  18410  blin2  18412  neibl  18484  blnei  18485  metss  18491  metss2lem  18494  stdbdmet  18499  stdbdmopn  18501  mopnex  18502  metrest  18507  prdsxmslem2  18512  metcnp3  18523  metcnp  18524  metcnpi3  18529  txmetcnp  18530  metustidOLD  18542  metustid  18543  cfilucfilOLD  18552  cfilucfil  18553  blval2  18558  elbl4  18559  metucnOLD  18571  metucn  18572  dscopn  18574  nmoix  18716  xrsmopn  18796  zdis  18800  reperflem  18802  reconnlem2  18811  metdseq0  18837  cnllycmp  18934  lebnum  18942  xlebnum  18943  lebnumii  18944  nmhmcn  19081  lmmbr  19164  lmmbr2  19165  lmnn  19169  cfilfcls  19180  iscau2  19183  iscmet3lem2  19198  equivcfil  19205  flimcfil  19219  cmpcmet  19223  cncmet  19228  bcthlem5  19234  ellimc3  19719  abelthlem2  20301  abelthlem5  20304  abelthlem7  20307  pige3  20378  dvlog2  20497  efopnlem1  20500  efopnlem2  20501  efopn  20502  logtayl  20504  logtayl2  20506  xrlimcnp  20760  efrlim  20761  pntlemi  21251  pntlemp  21257  nvelbl  22138  ubthlem1  22325  xdivpnfrp  24132  pnfinf  24206  lgamcvg2  24792  cnllyscon  24885  itg2gt0cn  26159  areacirclem2  26181  areacirclem3  26182  areacirc  26187  blssp  26352  sstotbnd2  26373  isbndx  26381  isbnd2  26382  isbnd3  26383  ssbnd  26387  prdstotbnd  26393  prdsbnd2  26394  cntotbnd  26395  ismtybndlem  26405  heibor1  26409  modelico  26774  sgnrrp  28235
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-un 3285  df-in 3287  df-ss 3294  df-xr 9080  df-rp 10569
  Copyright terms: Public domain W3C validator