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

Theorem rpxr 11792
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 11791 . 2 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
21rexrd 10041 1 (𝐴 ∈ ℝ+𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  *cxr 10025  +crp 11784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3191  df-un 3564  df-in 3566  df-ss 3573  df-xr 10030  df-rp 11785
This theorem is referenced by:  xlemul1  12071  xlemul2  12072  xltmul1  12073  xltmul2  12074  modelico  12628  muladdmodid  12658  sgnrrp  13773  blcntrps  22140  blcntr  22141  unirnblps  22147  unirnbl  22148  blssexps  22154  blssex  22155  blin2  22157  neibl  22229  blnei  22230  metss  22236  metss2lem  22239  stdbdmet  22244  stdbdmopn  22246  mopnex  22247  metrest  22252  prdsxmslem2  22257  metcnp3  22268  metcnp  22269  metcnpi3  22274  txmetcnp  22275  metustid  22282  cfilucfil  22287  blval2  22290  elbl4  22291  metucn  22299  dscopn  22301  nmoix  22456  xrsmopn  22538  zdis  22542  reperflem  22544  reconnlem2  22553  metdseq0  22580  cnllycmp  22678  lebnum  22686  xlebnum  22687  lebnumii  22688  nmhmcn  22843  lmmbr  22979  lmmbr2  22980  lmnn  22984  cfilfcls  22995  iscau2  22998  iscmet3lem2  23013  equivcfil  23020  flimcfil  23035  cmpcmet  23039  cncmet  23042  bcthlem5  23048  ellimc3  23566  abelthlem2  24107  abelthlem5  24110  abelthlem7  24113  pige3  24190  dvlog2  24316  efopnlem1  24319  efopnlem2  24320  efopn  24321  logtayl  24323  logtayl2  24325  xrlimcnp  24612  efrlim  24613  lgamcvg2  24698  pntlemi  25210  pntlemp  25216  ubthlem1  27596  xdivpnfrp  29450  pnfinf  29546  signsply0  30432  cnllysconn  30970  poimirlem29  33105  heicant  33111  itg2gt0cn  33132  ftc1anc  33160  areacirclem1  33167  areacirc  33172  blssp  33219  sstotbnd2  33240  isbndx  33248  isbnd2  33249  isbnd3  33250  ssbnd  33254  prdstotbnd  33260  prdsbnd2  33261  cntotbnd  33262  ismtybndlem  33272  heibor1  33276  infleinflem1  39081  limcrecl  39293  islpcn  39303  etransclem18  39802  etransclem46  39830  ioorrnopnlem  39857  sge0iunmptlemre  39965
  Copyright terms: Public domain W3C validator