Theorem rpxrd 12987

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝ^*cxr 11178  ℝ⁺crp 12942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-un 3894  df-ss 3906  df-xr 11183  df-rp 12943

This theorem is referenced by:  ssblex  24393  metequiv2  24475  metss2lem  24476  methaus  24485  met1stc  24486  met2ndci  24487  metcnp  24506  metcnpi3  24511  metustexhalf  24521  blval2  24527  metuel2  24530  nmoi2  24695  metdcnlem  24802  metdscnlem  24821  metnrmlem2  24826  metnrmlem3  24827  cnheibor  24922  cnllycmp  24923  lebnumlem3  24930  nmoleub2lem  25081  nmhmcn  25087  iscfil2  25233  cfil3i  25236  iscfil3  25240  cfilfcls  25241  iscmet3lem2  25259  caubl  25275  caublcls  25276  relcmpcmet  25285  bcthlem2  25292  bcthlem4  25294  bcthlem5  25295  ellimc3  25846  ftc1a  26004  ulmdvlem1  26365  psercnlem2  26389  psercn  26391  pserdvlem2  26393  pserdv  26394  efopn  26622  logccv  26627  efrlim  26933  lgamucov  27001  ftalem3  27038  logexprlim  27188  pntpbnd1a  27548  pntleme  27571  pntlem3  27572  pntleml  27574  ubthlem1  30941  ubthlem2  30942  sgnmulrp2  32909  tpr2rico  34056  xrmulc1cn  34074  omssubadd  34444  ptrecube  37941  poimirlem29  37970  heicant  37976  ftc1anclem6  38019  ftc1anclem7  38020  sstotbnd2  38095  equivtotbnd  38099  totbndbnd  38110  cntotbnd  38117  heibor1lem  38130  heiborlem3  38134  heiborlem6  38137  heiborlem8  38139  supxrge  45768  infrpge  45781  infleinflem1  45799  stoweid  46491  qndenserrnbl  46723  sge0rpcpnf  46849  sge0xaddlem1  46861