Theorem rpxrd 13013

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

Syntax hints:   → wi 4   ∈ wcel 2098  ℝ^*cxr 11243  ℝ⁺crp 12970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-un 3945  df-in 3947  df-ss 3957  df-xr 11248  df-rp 12971

This theorem is referenced by:  ssblex  24255  metequiv2  24340  metss2lem  24341  methaus  24350  met1stc  24351  met2ndci  24352  metcnp  24371  metcnpi3  24376  metustexhalf  24386  blval2  24392  metuel2  24395  nmoi2  24568  metdcnlem  24673  metdscnlem  24692  metnrmlem2  24697  metnrmlem3  24698  cnheibor  24802  cnllycmp  24803  lebnumlem3  24810  nmoleub2lem  24962  nmhmcn  24968  iscfil2  25115  cfil3i  25118  iscfil3  25122  cfilfcls  25123  iscmet3lem2  25141  caubl  25157  caublcls  25158  relcmpcmet  25167  bcthlem2  25174  bcthlem4  25176  bcthlem5  25177  ellimc3  25729  ftc1a  25893  ulmdvlem1  26252  psercnlem2  26277  psercn  26279  pserdvlem2  26281  pserdv  26282  efopn  26507  logccv  26512  efrlim  26816  efrlimOLD  26817  lgamucov  26885  ftalem3  26922  logexprlim  27073  pntpbnd1a  27433  pntleme  27456  pntlem3  27457  pntleml  27459  ubthlem1  30558  ubthlem2  30559  tpr2rico  33347  xrmulc1cn  33365  omssubadd  33754  sgnmulrp2  33997  ptrecube  36944  poimirlem29  36973  heicant  36979  ftc1anclem6  37022  ftc1anclem7  37023  sstotbnd2  37098  equivtotbnd  37102  totbndbnd  37113  cntotbnd  37120  heibor1lem  37133  heiborlem3  37137  heiborlem6  37140  heiborlem8  37142  supxrge  44499  infrpge  44512  infleinflem1  44531  stoweid  45230  qndenserrnbl  45462  sge0rpcpnf  45588  sge0xaddlem1  45600