Theorem rpxrd 12702

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝ^*cxr 10939  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-xr 10944  df-rp 12660

This theorem is referenced by:  ssblex  23489  metequiv2  23572  metss2lem  23573  methaus  23582  met1stc  23583  met2ndci  23584  metcnp  23603  metcnpi3  23608  metustexhalf  23618  blval2  23624  metuel2  23627  nmoi2  23800  metdcnlem  23905  metdscnlem  23924  metnrmlem2  23929  metnrmlem3  23930  cnheibor  24024  cnllycmp  24025  lebnumlem3  24032  nmoleub2lem  24183  nmhmcn  24189  iscfil2  24335  cfil3i  24338  iscfil3  24342  cfilfcls  24343  iscmet3lem2  24361  caubl  24377  caublcls  24378  relcmpcmet  24387  bcthlem2  24394  bcthlem4  24396  bcthlem5  24397  ellimc3  24948  ftc1a  25106  ulmdvlem1  25464  psercnlem2  25488  psercn  25490  pserdvlem2  25492  pserdv  25493  efopn  25718  logccv  25723  efrlim  26024  lgamucov  26092  ftalem3  26129  logexprlim  26278  pntpbnd1a  26638  pntleme  26661  pntlem3  26662  pntleml  26664  ubthlem1  29133  ubthlem2  29134  tpr2rico  31764  xrmulc1cn  31782  omssubadd  32167  sgnmulrp2  32410  ptrecube  35704  poimirlem29  35733  heicant  35739  ftc1anclem6  35782  ftc1anclem7  35783  sstotbnd2  35859  equivtotbnd  35863  totbndbnd  35874  cntotbnd  35881  heibor1lem  35894  heiborlem3  35898  heiborlem6  35901  heiborlem8  35903  supxrge  42767  infrpge  42780  infleinflem1  42799  stoweid  43494  qndenserrnbl  43726  sge0rpcpnf  43849  sge0xaddlem1  43861