Theorem rpxrd 12972

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 12971	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3	2	rexrd 11200	1 ⊢ (𝜑 → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2109  ℝ^*cxr 11183  ℝ⁺crp 12927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-un 3916  df-ss 3928  df-xr 11188  df-rp 12928

This theorem is referenced by:  ssblex  24292  metequiv2  24374  metss2lem  24375  methaus  24384  met1stc  24385  met2ndci  24386  metcnp  24405  metcnpi3  24410  metustexhalf  24420  blval2  24426  metuel2  24429  nmoi2  24594  metdcnlem  24701  metdscnlem  24720  metnrmlem2  24725  metnrmlem3  24726  cnheibor  24830  cnllycmp  24831  lebnumlem3  24838  nmoleub2lem  24990  nmhmcn  24996  iscfil2  25142  cfil3i  25145  iscfil3  25149  cfilfcls  25150  iscmet3lem2  25168  caubl  25184  caublcls  25185  relcmpcmet  25194  bcthlem2  25201  bcthlem4  25203  bcthlem5  25204  ellimc3  25756  ftc1a  25920  ulmdvlem1  26285  psercnlem2  26310  psercn  26312  pserdvlem2  26314  pserdv  26315  efopn  26543  logccv  26548  efrlim  26855  efrlimOLD  26856  lgamucov  26924  ftalem3  26961  logexprlim  27112  pntpbnd1a  27472  pntleme  27495  pntlem3  27496  pntleml  27498  ubthlem1  30772  ubthlem2  30773  sgnmulrp2  32734  tpr2rico  33875  xrmulc1cn  33893  omssubadd  34264  ptrecube  37587  poimirlem29  37616  heicant  37622  ftc1anclem6  37665  ftc1anclem7  37666  sstotbnd2  37741  equivtotbnd  37745  totbndbnd  37756  cntotbnd  37763  heibor1lem  37776  heiborlem3  37780  heiborlem6  37783  heiborlem8  37785  supxrge  45307  infrpge  45320  infleinflem1  45339  stoweid  46034  qndenserrnbl  46266  sge0rpcpnf  46392  sge0xaddlem1  46404