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

Theorem rpxr 10611
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 10610 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21rexrd 9126 1  |-  ( A  e.  RR+  ->  A  e. 
RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   RR*cxr 9111   RR+crp 10604
This theorem is referenced by:  xlemul1  10861  xlemul2  10862  xltmul1  10863  xltmul2  10864  blcntrps  18434  blcntr  18435  unirnblps  18441  unirnbl  18442  blssexps  18448  blssex  18449  blin2  18451  neibl  18523  blnei  18524  metss  18530  metss2lem  18533  stdbdmet  18538  stdbdmopn  18540  mopnex  18541  metrest  18546  prdsxmslem2  18551  metcnp3  18562  metcnp  18563  metcnpi3  18568  txmetcnp  18569  metustidOLD  18581  metustid  18582  cfilucfilOLD  18591  cfilucfil  18592  blval2  18597  elbl4  18598  metucnOLD  18610  metucn  18611  dscopn  18613  nmoix  18755  xrsmopn  18835  zdis  18839  reperflem  18841  reconnlem2  18850  metdseq0  18876  cnllycmp  18973  lebnum  18981  xlebnum  18982  lebnumii  18983  nmhmcn  19120  lmmbr  19203  lmmbr2  19204  lmnn  19208  cfilfcls  19219  iscau2  19222  iscmet3lem2  19237  equivcfil  19244  flimcfil  19258  cmpcmet  19262  cncmet  19267  bcthlem5  19273  ellimc3  19758  abelthlem2  20340  abelthlem5  20343  abelthlem7  20346  pige3  20417  dvlog2  20536  efopnlem1  20539  efopnlem2  20540  efopn  20541  logtayl  20543  logtayl2  20545  xrlimcnp  20799  efrlim  20800  pntlemi  21290  pntlemp  21296  nvelbl  22177  ubthlem1  22364  xdivpnfrp  24171  pnfinf  24245  lgamcvg2  24831  cnllyscon  24924  itg2gt0cn  26250  ftc1anc  26278  areacirclem2  26282  areacirclem3  26283  areacirc  26288  blssp  26453  sstotbnd2  26474  isbndx  26482  isbnd2  26483  isbnd3  26484  ssbnd  26488  prdstotbnd  26494  prdsbnd2  26495  cntotbnd  26496  ismtybndlem  26506  heibor1  26510  modelico  26875  sgnrrp  28458
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-un 3317  df-in 3319  df-ss 3326  df-xr 9116  df-rp 10605
  Copyright terms: Public domain W3C validator