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

Theorem rpxr 12620
Description: A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
rpxr (𝐴 ∈ ℝ+𝐴 ∈ ℝ*)

Proof of Theorem rpxr
StepHypRef Expression
1 rpre 12619 . 2 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
21rexrd 10908 1 (𝐴 ∈ ℝ+𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  *cxr 10891  +crp 12611
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3071  df-v 3423  df-un 3886  df-in 3888  df-ss 3898  df-xr 10896  df-rp 12612
This theorem is referenced by:  xlemul1  12905  xlemul2  12906  xltmul1  12907  xltmul2  12908  modelico  13481  muladdmodid  13511  sgnrrp  14682  blcntrps  23337  blcntr  23338  blssexps  23351  blssex  23352  blin2  23354  neibl  23426  blnei  23427  metss  23433  metss2lem  23436  stdbdmet  23441  stdbdmopn  23443  metrest  23449  prdsxmslem2  23454  metcnp3  23465  metcnp  23466  metcnpi3  23471  txmetcnp  23472  metustid  23479  cfilucfil  23484  blval2  23487  elbl4  23488  metucn  23496  nmoix  23654  xrsmopn  23736  reperflem  23742  reconnlem2  23751  metdseq0  23778  cnllycmp  23880  lebnum  23888  xlebnum  23889  lebnumii  23890  nmhmcn  24044  lmmbr  24182  lmmbr2  24183  lmnn  24187  cfilfcls  24198  iscau2  24201  iscmet3lem2  24216  equivcfil  24223  flimcfil  24238  cmpcmet  24243  bcthlem5  24252  ellimc3  24803  pige3ALT  25436  efopnlem1  25571  efopnlem2  25572  efopn  25573  xrlimcnp  25878  efrlim  25879  lgamcvg2  25964  pntlemi  26512  pntlemp  26518  ubthlem1  28978  xdivpnfrp  30954  pnfinf  31183  signsply0  32269  cnllysconn  32946  poimirlem29  35573  heicant  35579  itg2gt0cn  35599  ftc1anc  35625  areacirclem1  35632  areacirc  35637  blssp  35681  sstotbnd2  35699  isbndx  35707  isbnd2  35708  isbnd3  35709  ssbnd  35713  prdstotbnd  35719  prdsbnd2  35720  cntotbnd  35721  ismtybndlem  35731  heibor1  35735  infleinflem1  42615  limcrecl  42876  islpcn  42886  etransclem18  43499  etransclem46  43527  ioorrnopnlem  43551  sge0iunmptlemre  43659  itscnhlinecirc02p  45835
  Copyright terms: Public domain W3C validator