Theorem rpxrd 12950

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝ^*cxr 11165  ℝ⁺crp 12905

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-un 3906  df-ss 3918  df-xr 11170  df-rp 12906

This theorem is referenced by:  ssblex  24372  metequiv2  24454  metss2lem  24455  methaus  24464  met1stc  24465  met2ndci  24466  metcnp  24485  metcnpi3  24490  metustexhalf  24500  blval2  24506  metuel2  24509  nmoi2  24674  metdcnlem  24781  metdscnlem  24800  metnrmlem2  24805  metnrmlem3  24806  cnheibor  24910  cnllycmp  24911  lebnumlem3  24918  nmoleub2lem  25070  nmhmcn  25076  iscfil2  25222  cfil3i  25225  iscfil3  25229  cfilfcls  25230  iscmet3lem2  25248  caubl  25264  caublcls  25265  relcmpcmet  25274  bcthlem2  25281  bcthlem4  25283  bcthlem5  25284  ellimc3  25836  ftc1a  26000  ulmdvlem1  26365  psercnlem2  26390  psercn  26392  pserdvlem2  26394  pserdv  26395  efopn  26623  logccv  26628  efrlim  26935  efrlimOLD  26936  lgamucov  27004  ftalem3  27041  logexprlim  27192  pntpbnd1a  27552  pntleme  27575  pntlem3  27576  pntleml  27578  ubthlem1  30945  ubthlem2  30946  sgnmulrp2  32917  tpr2rico  34069  xrmulc1cn  34087  omssubadd  34457  ptrecube  37821  poimirlem29  37850  heicant  37856  ftc1anclem6  37899  ftc1anclem7  37900  sstotbnd2  37975  equivtotbnd  37979  totbndbnd  37990  cntotbnd  37997  heibor1lem  38010  heiborlem3  38014  heiborlem6  38017  heiborlem8  38019  supxrge  45583  infrpge  45596  infleinflem1  45614  stoweid  46307  qndenserrnbl  46539  sge0rpcpnf  46665  sge0xaddlem1  46677