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

Theorem rpxrd 12420
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 12419 . 2 (𝜑𝐴 ∈ ℝ)
32rexrd 10679 1 (𝜑𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  *cxr 10662  +crp 12377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-un 3938  df-in 3940  df-ss 3949  df-xr 10667  df-rp 12378
This theorem is referenced by:  ssblex  22965  metequiv2  23047  metss2lem  23048  methaus  23057  met1stc  23058  met2ndci  23059  metcnp  23078  metcnpi3  23083  metustexhalf  23093  blval2  23099  metuel2  23102  nmoi2  23266  metdcnlem  23371  metdscnlem  23390  metnrmlem2  23395  metnrmlem3  23396  cnheibor  23486  cnllycmp  23487  lebnumlem3  23494  nmoleub2lem  23645  nmhmcn  23651  iscfil2  23796  cfil3i  23799  iscfil3  23803  cfilfcls  23804  iscmet3lem2  23822  caubl  23838  caublcls  23839  relcmpcmet  23848  bcthlem2  23855  bcthlem4  23857  bcthlem5  23858  ellimc3  24404  ftc1a  24561  ulmdvlem1  24915  psercnlem2  24939  psercn  24941  pserdvlem2  24943  pserdv  24944  efopn  25168  logccv  25173  efrlim  25474  lgamucov  25542  ftalem3  25579  logexprlim  25728  pntpbnd1a  26088  pntleme  26111  pntlem3  26112  pntleml  26114  ubthlem1  28574  ubthlem2  28575  tpr2rico  31054  xrmulc1cn  31072  omssubadd  31457  sgnmulrp2  31700  ptrecube  34773  poimirlem29  34802  heicant  34808  ftc1anclem6  34853  ftc1anclem7  34854  sstotbnd2  34933  equivtotbnd  34937  totbndbnd  34948  cntotbnd  34955  heibor1lem  34968  heiborlem3  34972  heiborlem6  34975  heiborlem8  34977  supxrge  41482  infrpge  41495  infleinflem1  41514  stoweid  42225  qndenserrnbl  42457  sge0rpcpnf  42580  sge0xaddlem1  42592
  Copyright terms: Public domain W3C validator