Theorem rpxrd 12972

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝ^*cxr 11183  ℝ⁺crp 12927

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 3403  df-v 3446  df-un 3916  df-ss 3928  df-xr 11188  df-rp 12928

This theorem is referenced by:  ssblex  24349  metequiv2  24431  metss2lem  24432  methaus  24441  met1stc  24442  met2ndci  24443  metcnp  24462  metcnpi3  24467  metustexhalf  24477  blval2  24483  metuel2  24486  nmoi2  24651  metdcnlem  24758  metdscnlem  24777  metnrmlem2  24782  metnrmlem3  24783  cnheibor  24887  cnllycmp  24888  lebnumlem3  24895  nmoleub2lem  25047  nmhmcn  25053  iscfil2  25199  cfil3i  25202  iscfil3  25206  cfilfcls  25207  iscmet3lem2  25225  caubl  25241  caublcls  25242  relcmpcmet  25251  bcthlem2  25258  bcthlem4  25260  bcthlem5  25261  ellimc3  25813  ftc1a  25977  ulmdvlem1  26342  psercnlem2  26367  psercn  26369  pserdvlem2  26371  pserdv  26372  efopn  26600  logccv  26605  efrlim  26912  efrlimOLD  26913  lgamucov  26981  ftalem3  27018  logexprlim  27169  pntpbnd1a  27529  pntleme  27552  pntlem3  27553  pntleml  27555  ubthlem1  30849  ubthlem2  30850  sgnmulrp2  32811  tpr2rico  33895  xrmulc1cn  33913  omssubadd  34284  ptrecube  37607  poimirlem29  37636  heicant  37642  ftc1anclem6  37685  ftc1anclem7  37686  sstotbnd2  37761  equivtotbnd  37765  totbndbnd  37776  cntotbnd  37783  heibor1lem  37796  heiborlem3  37800  heiborlem6  37803  heiborlem8  37805  supxrge  45327  infrpge  45340  infleinflem1  45359  stoweid  46054  qndenserrnbl  46286  sge0rpcpnf  46412  sge0xaddlem1  46424