Theorem rpxrd 12420

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝ^*cxr 10663  ℝ⁺crp 12377

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-xr 10668  df-rp 12378

This theorem is referenced by:  ssblex  23035  metequiv2  23117  metss2lem  23118  methaus  23127  met1stc  23128  met2ndci  23129  metcnp  23148  metcnpi3  23153  metustexhalf  23163  blval2  23169  metuel2  23172  nmoi2  23336  metdcnlem  23441  metdscnlem  23460  metnrmlem2  23465  metnrmlem3  23466  cnheibor  23560  cnllycmp  23561  lebnumlem3  23568  nmoleub2lem  23719  nmhmcn  23725  iscfil2  23870  cfil3i  23873  iscfil3  23877  cfilfcls  23878  iscmet3lem2  23896  caubl  23912  caublcls  23913  relcmpcmet  23922  bcthlem2  23929  bcthlem4  23931  bcthlem5  23932  ellimc3  24482  ftc1a  24640  ulmdvlem1  24995  psercnlem2  25019  psercn  25021  pserdvlem2  25023  pserdv  25024  efopn  25249  logccv  25254  efrlim  25555  lgamucov  25623  ftalem3  25660  logexprlim  25809  pntpbnd1a  26169  pntleme  26192  pntlem3  26193  pntleml  26195  ubthlem1  28653  ubthlem2  28654  tpr2rico  31265  xrmulc1cn  31283  omssubadd  31668  sgnmulrp2  31911  ptrecube  35057  poimirlem29  35086  heicant  35092  ftc1anclem6  35135  ftc1anclem7  35136  sstotbnd2  35212  equivtotbnd  35216  totbndbnd  35227  cntotbnd  35234  heibor1lem  35247  heiborlem3  35251  heiborlem6  35254  heiborlem8  35256  supxrge  41970  infrpge  41983  infleinflem1  42002  stoweid  42705  qndenserrnbl  42937  sge0rpcpnf  43060  sge0xaddlem1  43072