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

Theorem rpxr 10361
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 10360 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21rexrd 8881 1  |-  ( A  e.  RR+  ->  A  e. 
RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   RR*cxr 8866   RR+crp 10354
This theorem is referenced by:  xlemul1  10610  xlemul2  10611  xltmul1  10612  xltmul2  10613  blcntr  17964  unirnbl  17969  blssex  17973  blin2  17975  neibl  18047  blnei  18048  metss  18054  metss2lem  18057  stdbdmet  18062  stdbdmopn  18064  mopnex  18065  metrest  18070  prdsxmslem2  18075  metcnp3  18086  metcnp  18087  metcnpi3  18092  txmetcnp  18093  dscopn  18096  nmoix  18238  xrsmopn  18318  zdis  18322  reperflem  18323  reconnlem2  18332  metdseq0  18358  cnllycmp  18454  lebnum  18462  xlebnum  18463  lebnumii  18464  nmhmcn  18601  lmmbr  18684  lmmbr2  18685  lmnn  18689  cfilfcls  18700  iscau2  18703  iscmet3lem2  18718  equivcfil  18725  flimcfil  18739  cmpcmet  18743  cncmet  18744  bcthlem5  18750  ellimc3  19229  abelthlem2  19808  abelthlem5  19811  abelthlem7  19814  pige3  19885  dvlog2  20000  efopnlem1  20003  efopnlem2  20004  efopn  20005  logtayl  20007  logtayl2  20009  xrlimcnp  20263  efrlim  20264  pntlemi  20753  pntlemp  20759  nvelbl  21262  ubthlem1  21449  xdivpnfrp  23117  cnllyscon  23776  areacirclem2  24925  areacirclem3  24926  areacirc  24931  blssp  26470  sstotbnd2  26498  equivtotbnd  26502  isbndx  26506  isbnd2  26507  isbnd3  26508  ssbnd  26512  prdstotbnd  26518  prdsbnd2  26519  cntotbnd  26520  ismtybndlem  26530  heibor1  26534  modelico  26906  stoweid  27812  sgnrrp  28248
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-xr 8871  df-rp 10355
  Copyright terms: Public domain W3C validator