Theorem rpxrd 12938

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝ^*cxr 11148  ℝ⁺crp 12893

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-un 3908  df-ss 3920  df-xr 11153  df-rp 12894

This theorem is referenced by:  ssblex  24314  metequiv2  24396  metss2lem  24397  methaus  24406  met1stc  24407  met2ndci  24408  metcnp  24427  metcnpi3  24432  metustexhalf  24442  blval2  24448  metuel2  24451  nmoi2  24616  metdcnlem  24723  metdscnlem  24742  metnrmlem2  24747  metnrmlem3  24748  cnheibor  24852  cnllycmp  24853  lebnumlem3  24860  nmoleub2lem  25012  nmhmcn  25018  iscfil2  25164  cfil3i  25167  iscfil3  25171  cfilfcls  25172  iscmet3lem2  25190  caubl  25206  caublcls  25207  relcmpcmet  25216  bcthlem2  25223  bcthlem4  25225  bcthlem5  25226  ellimc3  25778  ftc1a  25942  ulmdvlem1  26307  psercnlem2  26332  psercn  26334  pserdvlem2  26336  pserdv  26337  efopn  26565  logccv  26570  efrlim  26877  efrlimOLD  26878  lgamucov  26946  ftalem3  26983  logexprlim  27134  pntpbnd1a  27494  pntleme  27517  pntlem3  27518  pntleml  27520  ubthlem1  30814  ubthlem2  30815  sgnmulrp2  32781  tpr2rico  33879  xrmulc1cn  33897  omssubadd  34268  ptrecube  37604  poimirlem29  37633  heicant  37639  ftc1anclem6  37682  ftc1anclem7  37683  sstotbnd2  37758  equivtotbnd  37762  totbndbnd  37773  cntotbnd  37780  heibor1lem  37793  heiborlem3  37797  heiborlem6  37800  heiborlem8  37802  supxrge  45322  infrpge  45335  infleinflem1  45353  stoweid  46048  qndenserrnbl  46280  sge0rpcpnf  46406  sge0xaddlem1  46418