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

Theorem rpxrd 12959
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 12958 . 2 (𝜑𝐴 ∈ ℝ)
32rexrd 11206 1 (𝜑𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  *cxr 11189  +crp 12916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-un 3916  df-in 3918  df-ss 3928  df-xr 11194  df-rp 12917
This theorem is referenced by:  ssblex  23784  metequiv2  23869  metss2lem  23870  methaus  23879  met1stc  23880  met2ndci  23881  metcnp  23900  metcnpi3  23905  metustexhalf  23915  blval2  23921  metuel2  23924  nmoi2  24097  metdcnlem  24202  metdscnlem  24221  metnrmlem2  24226  metnrmlem3  24227  cnheibor  24321  cnllycmp  24322  lebnumlem3  24329  nmoleub2lem  24480  nmhmcn  24486  iscfil2  24633  cfil3i  24636  iscfil3  24640  cfilfcls  24641  iscmet3lem2  24659  caubl  24675  caublcls  24676  relcmpcmet  24685  bcthlem2  24692  bcthlem4  24694  bcthlem5  24695  ellimc3  25246  ftc1a  25404  ulmdvlem1  25762  psercnlem2  25786  psercn  25788  pserdvlem2  25790  pserdv  25791  efopn  26016  logccv  26021  efrlim  26322  lgamucov  26390  ftalem3  26427  logexprlim  26576  pntpbnd1a  26936  pntleme  26959  pntlem3  26960  pntleml  26962  ubthlem1  29815  ubthlem2  29816  tpr2rico  32496  xrmulc1cn  32514  omssubadd  32903  sgnmulrp2  33146  ptrecube  36081  poimirlem29  36110  heicant  36116  ftc1anclem6  36159  ftc1anclem7  36160  sstotbnd2  36236  equivtotbnd  36240  totbndbnd  36251  cntotbnd  36258  heibor1lem  36271  heiborlem3  36275  heiborlem6  36278  heiborlem8  36280  supxrge  43579  infrpge  43592  infleinflem1  43611  stoweid  44311  qndenserrnbl  44543  sge0rpcpnf  44669  sge0xaddlem1  44681
  Copyright terms: Public domain W3C validator