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

Theorem rpxrd 12426
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 12425 . 2 (𝜑𝐴 ∈ ℝ)
32rexrd 10685 1 (𝜑𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  *cxr 10668  +crp 12383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-un 3940  df-in 3942  df-ss 3951  df-xr 10673  df-rp 12384
This theorem is referenced by:  ssblex  23032  metequiv2  23114  metss2lem  23115  methaus  23124  met1stc  23125  met2ndci  23126  metcnp  23145  metcnpi3  23150  metustexhalf  23160  blval2  23166  metuel2  23169  nmoi2  23333  metdcnlem  23438  metdscnlem  23457  metnrmlem2  23462  metnrmlem3  23463  cnheibor  23553  cnllycmp  23554  lebnumlem3  23561  nmoleub2lem  23712  nmhmcn  23718  iscfil2  23863  cfil3i  23866  iscfil3  23870  cfilfcls  23871  iscmet3lem2  23889  caubl  23905  caublcls  23906  relcmpcmet  23915  bcthlem2  23922  bcthlem4  23924  bcthlem5  23925  ellimc3  24471  ftc1a  24628  ulmdvlem1  24982  psercnlem2  25006  psercn  25008  pserdvlem2  25010  pserdv  25011  efopn  25235  logccv  25240  efrlim  25541  lgamucov  25609  ftalem3  25646  logexprlim  25795  pntpbnd1a  26155  pntleme  26178  pntlem3  26179  pntleml  26181  ubthlem1  28641  ubthlem2  28642  tpr2rico  31150  xrmulc1cn  31168  omssubadd  31553  sgnmulrp2  31796  ptrecube  34886  poimirlem29  34915  heicant  34921  ftc1anclem6  34966  ftc1anclem7  34967  sstotbnd2  35046  equivtotbnd  35050  totbndbnd  35061  cntotbnd  35068  heibor1lem  35081  heiborlem3  35085  heiborlem6  35088  heiborlem8  35090  supxrge  41599  infrpge  41612  infleinflem1  41631  stoweid  42342  qndenserrnbl  42574  sge0rpcpnf  42697  sge0xaddlem1  42709
  Copyright terms: Public domain W3C validator