Theorem rpxrd 12773

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

Step	Hyp	Ref	Expression
1		rpred.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ+)
2	1	rpred 12772	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	rexrd 11025	1 ⊢ (𝜑 → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2106  ℝ^*cxr 11008  ℝ⁺crp 12730

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-xr 11013  df-rp 12731

This theorem is referenced by:  ssblex  23581  metequiv2  23666  metss2lem  23667  methaus  23676  met1stc  23677  met2ndci  23678  metcnp  23697  metcnpi3  23702  metustexhalf  23712  blval2  23718  metuel2  23721  nmoi2  23894  metdcnlem  23999  metdscnlem  24018  metnrmlem2  24023  metnrmlem3  24024  cnheibor  24118  cnllycmp  24119  lebnumlem3  24126  nmoleub2lem  24277  nmhmcn  24283  iscfil2  24430  cfil3i  24433  iscfil3  24437  cfilfcls  24438  iscmet3lem2  24456  caubl  24472  caublcls  24473  relcmpcmet  24482  bcthlem2  24489  bcthlem4  24491  bcthlem5  24492  ellimc3  25043  ftc1a  25201  ulmdvlem1  25559  psercnlem2  25583  psercn  25585  pserdvlem2  25587  pserdv  25588  efopn  25813  logccv  25818  efrlim  26119  lgamucov  26187  ftalem3  26224  logexprlim  26373  pntpbnd1a  26733  pntleme  26756  pntlem3  26757  pntleml  26759  ubthlem1  29232  ubthlem2  29233  tpr2rico  31862  xrmulc1cn  31880  omssubadd  32267  sgnmulrp2  32510  ptrecube  35777  poimirlem29  35806  heicant  35812  ftc1anclem6  35855  ftc1anclem7  35856  sstotbnd2  35932  equivtotbnd  35936  totbndbnd  35947  cntotbnd  35954  heibor1lem  35967  heiborlem3  35971  heiborlem6  35974  heiborlem8  35976  supxrge  42877  infrpge  42890  infleinflem1  42909  stoweid  43604  qndenserrnbl  43836  sge0rpcpnf  43959  sge0xaddlem1  43971