Theorem rpxrd 13077

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℝ^*cxr 11257  ℝ⁺crp 13032

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-un 3911  df-ss 3923  df-xr 11262  df-rp 13033

This theorem is used by:  sgnmulrp2  15169  ssblex  24636  metequiv2  24718  metss2lem  24719  methaus  24728  met1stc  24729  met2ndci  24730  metcnp  24749  metcnpi3  24754  metustexhalf  24764  blval2  24770  metuel2  24773  nmoi2  24938  metdcnlem  25045  metdscnlem  25064  metnrmlem2  25069  metnrmlem3  25070  cnheibor  25165  cnllycmp  25166  lebnumlem3  25173  nmoleub2lem  25324  nmhmcn  25330  iscfil2  25476  cfil3i  25479  iscfil3  25483  cfilfcls  25484  iscmet3lem2  25502  caubl  25518  caublcls  25519  relcmpcmet  25528  bcthlem2  25535  bcthlem4  25537  bcthlem5  25538  ellimc3  26089  ftc1a  26247  ulmdvlem1  26614  psercnlem2  26638  psercn  26640  pserdvlem2  26642  pserdv  26643  efopn  26874  logccv  26879  efrlim  27185  lgamucov  27253  ftalem3  27290  logexprlim  27440  pntpbnd1a  27800  pntleme  27823  pntlem3  27824  pntleml  27826  ubthlem1  31293  ubthlem2  31294  tpr2rico  34366  xrmulc1cn  34384  omssubadd  34755  ptrecube  38328  poimirlem29  38357  heicant  38363  ftc1anclem6  38406  ftc1anclem7  38407  sstotbnd2  38483  equivtotbnd  38487  totbndbnd  38498  cntotbnd  38505  heibor1lem  38518  heiborlem3  38522  heiborlem6  38525  heiborlem8  38527  supxrge  46112  infrpge  46125  infleinflem1  46143  stoweid  46835  qndenserrnbl  47067  sge0rpcpnf  47193  sge0xaddlem1  47205