Theorem rpxrd 13003

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝ^*cxr 11214  ℝ⁺crp 12958

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-un 3922  df-ss 3934  df-xr 11219  df-rp 12959

This theorem is referenced by:  ssblex  24323  metequiv2  24405  metss2lem  24406  methaus  24415  met1stc  24416  met2ndci  24417  metcnp  24436  metcnpi3  24441  metustexhalf  24451  blval2  24457  metuel2  24460  nmoi2  24625  metdcnlem  24732  metdscnlem  24751  metnrmlem2  24756  metnrmlem3  24757  cnheibor  24861  cnllycmp  24862  lebnumlem3  24869  nmoleub2lem  25021  nmhmcn  25027  iscfil2  25173  cfil3i  25176  iscfil3  25180  cfilfcls  25181  iscmet3lem2  25199  caubl  25215  caublcls  25216  relcmpcmet  25225  bcthlem2  25232  bcthlem4  25234  bcthlem5  25235  ellimc3  25787  ftc1a  25951  ulmdvlem1  26316  psercnlem2  26341  psercn  26343  pserdvlem2  26345  pserdv  26346  efopn  26574  logccv  26579  efrlim  26886  efrlimOLD  26887  lgamucov  26955  ftalem3  26992  logexprlim  27143  pntpbnd1a  27503  pntleme  27526  pntlem3  27527  pntleml  27529  ubthlem1  30806  ubthlem2  30807  sgnmulrp2  32768  tpr2rico  33909  xrmulc1cn  33927  omssubadd  34298  ptrecube  37621  poimirlem29  37650  heicant  37656  ftc1anclem6  37699  ftc1anclem7  37700  sstotbnd2  37775  equivtotbnd  37779  totbndbnd  37790  cntotbnd  37797  heibor1lem  37810  heiborlem3  37814  heiborlem6  37817  heiborlem8  37819  supxrge  45341  infrpge  45354  infleinflem1  45373  stoweid  46068  qndenserrnbl  46300  sge0rpcpnf  46426  sge0xaddlem1  46438