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

Theorem rpxr 10551
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 10550 . 2  |-  ( A  e.  RR+  ->  A  e.  RR )
21rexrd 9067 1  |-  ( A  e.  RR+  ->  A  e. 
RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   RR*cxr 9052   RR+crp 10544
This theorem is referenced by:  xlemul1  10801  xlemul2  10802  xltmul1  10803  xltmul2  10804  blcntr  18338  unirnbl  18343  blssex  18347  blin2  18349  neibl  18421  blnei  18422  metss  18428  metss2lem  18431  stdbdmet  18436  stdbdmopn  18438  mopnex  18439  metrest  18444  prdsxmslem2  18449  metcnp3  18460  metcnp  18461  metcnpi3  18466  txmetcnp  18467  metustid  18474  cfilucfil  18479  blval2  18482  elbl4  18483  metucn  18490  dscopn  18492  nmoix  18634  xrsmopn  18714  zdis  18718  reperflem  18720  reconnlem2  18729  metdseq0  18755  cnllycmp  18852  lebnum  18860  xlebnum  18861  lebnumii  18862  nmhmcn  18999  lmmbr  19082  lmmbr2  19083  lmnn  19087  cfilfcls  19098  iscau2  19101  iscmet3lem2  19116  equivcfil  19123  flimcfil  19137  cmpcmet  19141  cncmet  19144  bcthlem5  19150  ellimc3  19633  abelthlem2  20215  abelthlem5  20218  abelthlem7  20221  pige3  20292  dvlog2  20411  efopnlem1  20414  efopnlem2  20415  efopn  20416  logtayl  20418  logtayl2  20420  xrlimcnp  20674  efrlim  20675  pntlemi  21165  pntlemp  21171  nvelbl  22033  ubthlem1  22220  xdivpnfrp  24018  lgamcvg2  24618  cnllyscon  24711  itg2gt0cn  25960  areacirclem2  25982  areacirclem3  25983  areacirc  25988  blssp  26153  sstotbnd2  26174  isbndx  26182  isbnd2  26183  isbnd3  26184  ssbnd  26188  prdstotbnd  26194  prdsbnd2  26195  cntotbnd  26196  ismtybndlem  26206  heibor1  26210  modelico  26575  sgnrrp  27867
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rab 2658  df-v 2901  df-un 3268  df-in 3270  df-ss 3277  df-xr 9057  df-rp 10545
  Copyright terms: Public domain W3C validator