Theorem rpxrd 13038

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

Syntax hints:   → wi 4   ∈ wcel 2142  ℝ^*cxr 11215  ℝ⁺crp 12993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-un 3909  df-ss 3921  df-xr 11220  df-rp 12994

This theorem is referenced by:  sgnmulrp2  15121  ssblex  24488  metequiv2  24570  metss2lem  24571  methaus  24580  met1stc  24581  met2ndci  24582  metcnp  24601  metcnpi3  24606  metustexhalf  24616  blval2  24622  metuel2  24625  nmoi2  24790  metdcnlem  24897  metdscnlem  24916  metnrmlem2  24921  metnrmlem3  24922  cnheibor  25017  cnllycmp  25018  lebnumlem3  25025  nmoleub2lem  25176  nmhmcn  25182  iscfil2  25328  cfil3i  25331  iscfil3  25335  cfilfcls  25336  iscmet3lem2  25354  caubl  25370  caublcls  25371  relcmpcmet  25380  bcthlem2  25387  bcthlem4  25389  bcthlem5  25390  ellimc3  25941  ftc1a  26099  ulmdvlem1  26463  psercnlem2  26487  psercn  26489  pserdvlem2  26491  pserdv  26492  efopn  26723  logccv  26728  efrlim  27034  lgamucov  27102  ftalem3  27139  logexprlim  27289  pntpbnd1a  27649  pntleme  27672  pntlem3  27673  pntleml  27675  ubthlem1  31073  ubthlem2  31074  tpr2rico  34209  xrmulc1cn  34227  omssubadd  34597  ptrecube  38119  poimirlem29  38148  heicant  38154  ftc1anclem6  38197  ftc1anclem7  38198  sstotbnd2  38273  equivtotbnd  38277  totbndbnd  38288  cntotbnd  38295  heibor1lem  38308  heiborlem3  38312  heiborlem6  38315  heiborlem8  38317  supxrge  45914  infrpge  45927  infleinflem1  45945  stoweid  46637  qndenserrnbl  46869  sge0rpcpnf  46995  sge0xaddlem1  47007