Theorem rpxrd 11031

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

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 |- ( ph -> A e. RR+ )
2	1	rpred 11030	. 2 |- ( ph -> A e. RR )
3	2	rexrd 9436	1 |- ( ph -> A e. RR* )

Syntax hints:   -> wi 4   e. wcel 1756   RR*cxr 9420   RR+crp 10994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-rab 2727  df-v 2977  df-un 3336  df-in 3338  df-ss 3345  df-xr 9425  df-rp 10995

This theorem is referenced by:  ssblex  20006  metequiv2  20088  metss2lem  20089  methaus  20098  met1stc  20099  met2ndci  20100  metcnp  20119  metcnpi3  20124  metustexhalfOLD  20141  metustexhalf  20142  blval2  20153  metuel2  20157  nmoi2  20312  metdcnlem  20416  metdscnlem  20434  metnrmlem2  20439  metnrmlem3  20440  cnheibor  20530  cnllycmp  20531  lebnumlem3  20538  nmoleub2lem  20672  nmhmcn  20678  iscfil2  20780  cfil3i  20783  iscfil3  20787  iscmet3lem2  20806  caubl  20821  caublcls  20822  relcmpcmet  20830  bcthlem2  20839  bcthlem4  20841  bcthlem5  20842  ellimc3  21357  ftc1a  21512  ulmdvlem1  21868  psercnlem2  21892  psercn  21894  pserdvlem2  21896  pserdv  21897  efopn  22106  logccv  22111  efrlim  22366  ftalem3  22415  logexprlim  22567  pntpbnd1a  22837  pntleme  22860  pntlem3  22861  pntleml  22863  ubthlem1  24274  ubthlem2  24275  tpr2rico  26345  xrmulc1cn  26363  lgamucov  27027  heicant  28429  ftc1anclem6  28475  ftc1anclem7  28476  sstotbnd2  28676  equivtotbnd  28680  totbndbnd  28691  cntotbnd  28698  heibor1lem  28711  heiborlem3  28715  heiborlem6  28718  heiborlem8  28720  stoweid  29861