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

Theorem rpxrd 10391
Description: A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1  |-  ( ph  ->  A  e.  RR+ )
Assertion
Ref Expression
rpxrd  |-  ( ph  ->  A  e.  RR* )

Proof of Theorem rpxrd
StepHypRef Expression
1 rpred.1 . . 3  |-  ( ph  ->  A  e.  RR+ )
21rpred 10390 . 2  |-  ( ph  ->  A  e.  RR )
32rexrd 8881 1  |-  ( ph  ->  A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   RR*cxr 8866   RR+crp 10354
This theorem is referenced by:  ssblex  17974  metequiv2  18056  metss2lem  18057  methaus  18066  met1stc  18067  met2ndci  18068  metcnp  18087  metcnpi3  18092  nmoi2  18239  metdcnlem  18341  metdscnlem  18359  metnrmlem2  18364  metnrmlem3  18365  cnheibor  18453  cnllycmp  18454  lebnumlem3  18461  nmoleub2lem  18595  nmhmcn  18601  iscfil2  18692  cfil3i  18695  iscfil3  18699  iscmet3lem2  18718  caubl  18733  caublcls  18734  relcmpcmet  18742  bcthlem2  18747  bcthlem4  18749  bcthlem5  18750  ellimc3  19229  ftc1a  19384  ulmdvlem1  19777  psercnlem2  19800  psercn  19802  pserdvlem2  19804  pserdv  19805  efopn  20005  logccv  20010  efrlim  20264  ftalem3  20312  logexprlim  20464  pntpbnd1a  20734  pntleme  20757  pntlem3  20758  pntleml  20760  ubthlem1  21449  ubthlem2  21450  tpr2rico  23296  xrmulc1cn  23303  sstotbnd2  26498  totbndbnd  26513  heibor1lem  26533  heiborlem3  26537  heiborlem6  26540  heiborlem8  26542
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-xr 8871  df-rp 10355
  Copyright terms: Public domain W3C validator