Theorem rpxrd 13052

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝ^*cxr 11268  ℝ⁺crp 13008

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-un 3931  df-ss 3943  df-xr 11273  df-rp 13009

This theorem is referenced by:  ssblex  24367  metequiv2  24449  metss2lem  24450  methaus  24459  met1stc  24460  met2ndci  24461  metcnp  24480  metcnpi3  24485  metustexhalf  24495  blval2  24501  metuel2  24504  nmoi2  24669  metdcnlem  24776  metdscnlem  24795  metnrmlem2  24800  metnrmlem3  24801  cnheibor  24905  cnllycmp  24906  lebnumlem3  24913  nmoleub2lem  25065  nmhmcn  25071  iscfil2  25218  cfil3i  25221  iscfil3  25225  cfilfcls  25226  iscmet3lem2  25244  caubl  25260  caublcls  25261  relcmpcmet  25270  bcthlem2  25277  bcthlem4  25279  bcthlem5  25280  ellimc3  25832  ftc1a  25996  ulmdvlem1  26361  psercnlem2  26386  psercn  26388  pserdvlem2  26390  pserdv  26391  efopn  26619  logccv  26624  efrlim  26931  efrlimOLD  26932  lgamucov  27000  ftalem3  27037  logexprlim  27188  pntpbnd1a  27548  pntleme  27571  pntlem3  27572  pntleml  27574  ubthlem1  30851  ubthlem2  30852  sgnmulrp2  32815  tpr2rico  33943  xrmulc1cn  33961  omssubadd  34332  ptrecube  37644  poimirlem29  37673  heicant  37679  ftc1anclem6  37722  ftc1anclem7  37723  sstotbnd2  37798  equivtotbnd  37802  totbndbnd  37813  cntotbnd  37820  heibor1lem  37833  heiborlem3  37837  heiborlem6  37840  heiborlem8  37842  supxrge  45365  infrpge  45378  infleinflem1  45397  stoweid  46092  qndenserrnbl  46324  sge0rpcpnf  46450  sge0xaddlem1  46462