Theorem rpxrd 12962

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝ^*cxr 11177  ℝ⁺crp 12917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-un 3908  df-ss 3920  df-xr 11182  df-rp 12918

This theorem is referenced by:  ssblex  24384  metequiv2  24466  metss2lem  24467  methaus  24476  met1stc  24477  met2ndci  24478  metcnp  24497  metcnpi3  24502  metustexhalf  24512  blval2  24518  metuel2  24521  nmoi2  24686  metdcnlem  24793  metdscnlem  24812  metnrmlem2  24817  metnrmlem3  24818  cnheibor  24922  cnllycmp  24923  lebnumlem3  24930  nmoleub2lem  25082  nmhmcn  25088  iscfil2  25234  cfil3i  25237  iscfil3  25241  cfilfcls  25242  iscmet3lem2  25260  caubl  25276  caublcls  25277  relcmpcmet  25286  bcthlem2  25293  bcthlem4  25295  bcthlem5  25296  ellimc3  25848  ftc1a  26012  ulmdvlem1  26377  psercnlem2  26402  psercn  26404  pserdvlem2  26406  pserdv  26407  efopn  26635  logccv  26640  efrlim  26947  efrlimOLD  26948  lgamucov  27016  ftalem3  27053  logexprlim  27204  pntpbnd1a  27564  pntleme  27587  pntlem3  27588  pntleml  27590  ubthlem1  30958  ubthlem2  30959  sgnmulrp2  32928  tpr2rico  34090  xrmulc1cn  34108  omssubadd  34478  ptrecube  37871  poimirlem29  37900  heicant  37906  ftc1anclem6  37949  ftc1anclem7  37950  sstotbnd2  38025  equivtotbnd  38029  totbndbnd  38040  cntotbnd  38047  heibor1lem  38060  heiborlem3  38064  heiborlem6  38067  heiborlem8  38069  supxrge  45697  infrpge  45710  infleinflem1  45728  stoweid  46421  qndenserrnbl  46653  sge0rpcpnf  46779  sge0xaddlem1  46791