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

Theorem rpxr 12033
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 12032 . 2 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
21rexrd 10281 1 (𝐴 ∈ ℝ+𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  *cxr 10265  +crp 12025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-un 3720  df-in 3722  df-ss 3729  df-xr 10270  df-rp 12026
This theorem is referenced by:  xlemul1  12313  xlemul2  12314  xltmul1  12315  xltmul2  12316  modelico  12874  muladdmodid  12904  sgnrrp  14030  blcntrps  22418  blcntr  22419  unirnblps  22425  unirnbl  22426  blssexps  22432  blssex  22433  blin2  22435  neibl  22507  blnei  22508  metss  22514  metss2lem  22517  stdbdmet  22522  stdbdmopn  22524  mopnex  22525  metrest  22530  prdsxmslem2  22535  metcnp3  22546  metcnp  22547  metcnpi3  22552  txmetcnp  22553  metustid  22560  cfilucfil  22565  blval2  22568  elbl4  22569  metucn  22577  dscopn  22579  nmoix  22734  xrsmopn  22816  zdis  22820  reperflem  22822  reconnlem2  22831  metdseq0  22858  cnllycmp  22956  lebnum  22964  xlebnum  22965  lebnumii  22966  nmhmcn  23120  lmmbr  23256  lmmbr2  23257  lmnn  23261  cfilfcls  23272  iscau2  23275  iscmet3lem2  23290  equivcfil  23297  flimcfil  23312  cmpcmet  23316  cncmet  23319  bcthlem5  23325  ellimc3  23842  abelthlem2  24385  abelthlem5  24388  abelthlem7  24391  pige3  24468  dvlog2  24598  efopnlem1  24601  efopnlem2  24602  efopn  24603  logtayl  24605  logtayl2  24607  xrlimcnp  24894  efrlim  24895  lgamcvg2  24980  pntlemi  25492  pntlemp  25498  ubthlem1  28035  xdivpnfrp  29950  pnfinf  30046  signsply0  30937  cnllysconn  31534  poimirlem29  33751  heicant  33757  itg2gt0cn  33778  ftc1anc  33806  areacirclem1  33813  areacirc  33818  blssp  33865  sstotbnd2  33886  isbndx  33894  isbnd2  33895  isbnd3  33896  ssbnd  33900  prdstotbnd  33906  prdsbnd2  33907  cntotbnd  33908  ismtybndlem  33918  heibor1  33922  infleinflem1  40084  limcrecl  40364  islpcn  40374  etransclem18  40972  etransclem46  41000  ioorrnopnlem  41027  sge0iunmptlemre  41135
  Copyright terms: Public domain W3C validator