Theorem rpxrd 13075

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℝ^*cxr 11291  ℝ⁺crp 13031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-un 3967  df-ss 3979  df-xr 11296  df-rp 13032

This theorem is referenced by:  ssblex  24453  metequiv2  24538  metss2lem  24539  methaus  24548  met1stc  24549  met2ndci  24550  metcnp  24569  metcnpi3  24574  metustexhalf  24584  blval2  24590  metuel2  24593  nmoi2  24766  metdcnlem  24871  metdscnlem  24890  metnrmlem2  24895  metnrmlem3  24896  cnheibor  25000  cnllycmp  25001  lebnumlem3  25008  nmoleub2lem  25160  nmhmcn  25166  iscfil2  25313  cfil3i  25316  iscfil3  25320  cfilfcls  25321  iscmet3lem2  25339  caubl  25355  caublcls  25356  relcmpcmet  25365  bcthlem2  25372  bcthlem4  25374  bcthlem5  25375  ellimc3  25928  ftc1a  26092  ulmdvlem1  26457  psercnlem2  26482  psercn  26484  pserdvlem2  26486  pserdv  26487  efopn  26714  logccv  26719  efrlim  27026  efrlimOLD  27027  lgamucov  27095  ftalem3  27132  logexprlim  27283  pntpbnd1a  27643  pntleme  27666  pntlem3  27667  pntleml  27669  ubthlem1  30898  ubthlem2  30899  tpr2rico  33872  xrmulc1cn  33890  omssubadd  34281  sgnmulrp2  34524  ptrecube  37606  poimirlem29  37635  heicant  37641  ftc1anclem6  37684  ftc1anclem7  37685  sstotbnd2  37760  equivtotbnd  37764  totbndbnd  37775  cntotbnd  37782  heibor1lem  37795  heiborlem3  37799  heiborlem6  37802  heiborlem8  37804  supxrge  45287  infrpge  45300  infleinflem1  45319  stoweid  46018  qndenserrnbl  46250  sge0rpcpnf  46376  sge0xaddlem1  46388