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

Theorem rpxr 11238
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 11237 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21rexrd 9646 1  |-  ( A  e.  RR+  ->  A  e. 
RR* )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   RR*cxr 9630   RR+crp 11231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-un 3466  df-in 3468  df-ss 3475  df-xr 9635  df-rp 11232
This theorem is referenced by:  xlemul1  11493  xlemul2  11494  xltmul1  11495  xltmul2  11496  sgnrrp  12906  blcntrps  20893  blcntr  20894  unirnblps  20900  unirnbl  20901  blssexps  20907  blssex  20908  blin2  20910  neibl  20982  blnei  20983  metss  20989  metss2lem  20992  stdbdmet  20997  stdbdmopn  20999  mopnex  21000  metrest  21005  prdsxmslem2  21010  metcnp3  21021  metcnp  21022  metcnpi3  21027  txmetcnp  21028  metustidOLD  21040  metustid  21041  cfilucfilOLD  21050  cfilucfil  21051  blval2  21056  elbl4  21057  metucnOLD  21069  metucn  21070  dscopn  21072  nmoix  21214  xrsmopn  21295  zdis  21299  reperflem  21301  reconnlem2  21310  metdseq0  21336  cnllycmp  21434  lebnum  21442  xlebnum  21443  lebnumii  21444  nmhmcn  21581  lmmbr  21675  lmmbr2  21676  lmnn  21680  cfilfcls  21691  iscau2  21694  iscmet3lem2  21709  equivcfil  21716  flimcfil  21730  cmpcmet  21734  cncmet  21739  bcthlem5  21745  ellimc3  22261  abelthlem2  22805  abelthlem5  22808  abelthlem7  22811  pige3  22888  dvlog2  23012  efopnlem1  23015  efopnlem2  23016  efopn  23017  logtayl  23019  logtayl2  23021  xrlimcnp  23276  efrlim  23277  pntlemi  23767  pntlemp  23773  nvelbl  25577  ubthlem1  25764  xdivpnfrp  27607  pnfinf  27705  signsply0  28486  lgamcvg2  28575  cnllyscon  28668  heicant  30025  itg2gt0cn  30046  ftc1anc  30074  areacirclem1  30083  areacirc  30088  blssp  30225  sstotbnd2  30246  isbndx  30254  isbnd2  30255  isbnd3  30256  ssbnd  30260  prdstotbnd  30266  prdsbnd2  30267  cntotbnd  30268  ismtybndlem  30278  heibor1  30282  modelico  30733  limcrecl  31589  islpcn  31599  etransclem18  31989  etransclem46  32017
  Copyright terms: Public domain W3C validator