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

Theorem rpxr 10377
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 10376 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21rexrd 8897 1  |-  ( A  e.  RR+  ->  A  e. 
RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   RR*cxr 8882   RR+crp 10370
This theorem is referenced by:  xlemul1  10626  xlemul2  10627  xltmul1  10628  xltmul2  10629  blcntr  17980  unirnbl  17985  blssex  17989  blin2  17991  neibl  18063  blnei  18064  metss  18070  metss2lem  18073  stdbdmet  18078  stdbdmopn  18080  mopnex  18081  metrest  18086  prdsxmslem2  18091  metcnp3  18102  metcnp  18103  metcnpi3  18108  txmetcnp  18109  dscopn  18112  nmoix  18254  xrsmopn  18334  zdis  18338  reperflem  18339  reconnlem2  18348  metdseq0  18374  cnllycmp  18470  lebnum  18478  xlebnum  18479  lebnumii  18480  nmhmcn  18617  lmmbr  18700  lmmbr2  18701  lmnn  18705  cfilfcls  18716  iscau2  18719  iscmet3lem2  18734  equivcfil  18741  flimcfil  18755  cmpcmet  18759  cncmet  18760  bcthlem5  18766  ellimc3  19245  abelthlem2  19824  abelthlem5  19827  abelthlem7  19830  pige3  19901  dvlog2  20016  efopnlem1  20019  efopnlem2  20020  efopn  20021  logtayl  20023  logtayl2  20025  xrlimcnp  20279  efrlim  20280  pntlemi  20769  pntlemp  20775  nvelbl  21278  ubthlem1  21465  xdivpnfrp  23133  cnllyscon  23791  itg2gt0cn  25006  areacirclem2  25028  areacirclem3  25029  areacirc  25034  blssp  26573  sstotbnd2  26601  equivtotbnd  26605  isbndx  26609  isbnd2  26610  isbnd3  26611  ssbnd  26615  prdstotbnd  26621  prdsbnd2  26622  cntotbnd  26623  ismtybndlem  26633  heibor1  26637  modelico  27009  stoweid  27915  sgnrrp  28502
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-un 3170  df-in 3172  df-ss 3179  df-xr 8887  df-rp 10371
  Copyright terms: Public domain W3C validator