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

Theorem rpxrd 11817
Description: A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1 (𝜑𝐴 ∈ ℝ+)
Assertion
Ref Expression
rpxrd (𝜑𝐴 ∈ ℝ*)

Proof of Theorem rpxrd
StepHypRef Expression
1 rpred.1 . . 3 (𝜑𝐴 ∈ ℝ+)
21rpred 11816 . 2 (𝜑𝐴 ∈ ℝ)
32rexrd 10033 1 (𝜑𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  *cxr 10017  +crp 11776
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 3188  df-un 3560  df-in 3562  df-ss 3569  df-xr 10022  df-rp 11777
This theorem is referenced by:  ssblex  22143  metequiv2  22225  metss2lem  22226  methaus  22235  met1stc  22236  met2ndci  22237  metcnp  22256  metcnpi3  22261  metustexhalf  22271  blval2  22277  metuel2  22280  nmoi2  22444  metdcnlem  22547  metdscnlem  22566  metnrmlem2  22571  metnrmlem3  22572  cnheibor  22662  cnllycmp  22663  lebnumlem3  22670  nmoleub2lem  22822  nmhmcn  22828  iscfil2  22972  cfil3i  22975  iscfil3  22979  iscmet3lem2  22998  caubl  23014  caublcls  23015  relcmpcmet  23023  bcthlem2  23030  bcthlem4  23032  bcthlem5  23033  ellimc3  23549  ftc1a  23704  ulmdvlem1  24058  psercnlem2  24082  psercn  24084  pserdvlem2  24086  pserdv  24087  efopn  24304  logccv  24309  efrlim  24596  lgamucov  24664  ftalem3  24701  logexprlim  24850  pntpbnd1a  25174  pntleme  25197  pntlem3  25198  pntleml  25200  ubthlem1  27572  ubthlem2  27573  tpr2rico  29737  xrmulc1cn  29755  omssubadd  30140  sgnmulrp2  30383  ptrecube  33038  poimirlem29  33067  heicant  33073  ftc1anclem6  33119  ftc1anclem7  33120  sstotbnd2  33202  equivtotbnd  33206  totbndbnd  33217  cntotbnd  33224  heibor1lem  33237  heiborlem3  33241  heiborlem6  33244  heiborlem8  33246  supxrge  39015  infrpge  39028  infleinflem1  39047  stoweid  39584  qndenserrnbl  39819  sge0rpcpnf  39942  sge0xaddlem1  39954
  Copyright terms: Public domain W3C validator