Theorem rpxrd 12948

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝ^*cxr 11163  ℝ⁺crp 12903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-un 3904  df-ss 3916  df-xr 11168  df-rp 12904

This theorem is referenced by:  ssblex  24370  metequiv2  24452  metss2lem  24453  methaus  24462  met1stc  24463  met2ndci  24464  metcnp  24483  metcnpi3  24488  metustexhalf  24498  blval2  24504  metuel2  24507  nmoi2  24672  metdcnlem  24779  metdscnlem  24798  metnrmlem2  24803  metnrmlem3  24804  cnheibor  24908  cnllycmp  24909  lebnumlem3  24916  nmoleub2lem  25068  nmhmcn  25074  iscfil2  25220  cfil3i  25223  iscfil3  25227  cfilfcls  25228  iscmet3lem2  25246  caubl  25262  caublcls  25263  relcmpcmet  25272  bcthlem2  25279  bcthlem4  25281  bcthlem5  25282  ellimc3  25834  ftc1a  25998  ulmdvlem1  26363  psercnlem2  26388  psercn  26390  pserdvlem2  26392  pserdv  26393  efopn  26621  logccv  26626  efrlim  26933  efrlimOLD  26934  lgamucov  27002  ftalem3  27039  logexprlim  27190  pntpbnd1a  27550  pntleme  27573  pntlem3  27574  pntleml  27576  ubthlem1  30894  ubthlem2  30895  sgnmulrp2  32866  tpr2rico  34018  xrmulc1cn  34036  omssubadd  34406  ptrecube  37760  poimirlem29  37789  heicant  37795  ftc1anclem6  37838  ftc1anclem7  37839  sstotbnd2  37914  equivtotbnd  37918  totbndbnd  37929  cntotbnd  37936  heibor1lem  37949  heiborlem3  37953  heiborlem6  37956  heiborlem8  37958  supxrge  45525  infrpge  45538  infleinflem1  45556  stoweid  46249  qndenserrnbl  46481  sge0rpcpnf  46607  sge0xaddlem1  46619