Theorem rpxrd 12182

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝ^*cxr 10410  ℝ⁺crp 12137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-un 3797  df-in 3799  df-ss 3806  df-xr 10415  df-rp 12138

This theorem is referenced by:  ssblex  22641  metequiv2  22723  metss2lem  22724  methaus  22733  met1stc  22734  met2ndci  22735  metcnp  22754  metcnpi3  22759  metustexhalf  22769  blval2  22775  metuel2  22778  nmoi2  22942  metdcnlem  23047  metdscnlem  23066  metnrmlem2  23071  metnrmlem3  23072  cnheibor  23162  cnllycmp  23163  lebnumlem3  23170  nmoleub2lem  23321  nmhmcn  23327  iscfil2  23472  cfil3i  23475  iscfil3  23479  iscmet3lem2  23498  caubl  23514  caublcls  23515  relcmpcmet  23524  bcthlem2  23531  bcthlem4  23533  bcthlem5  23534  ellimc3  24080  ftc1a  24237  ulmdvlem1  24591  psercnlem2  24615  psercn  24617  pserdvlem2  24619  pserdv  24620  efopn  24841  logccv  24846  efrlim  25148  lgamucov  25216  ftalem3  25253  logexprlim  25402  pntpbnd1a  25726  pntleme  25749  pntlem3  25750  pntleml  25752  ubthlem1  28298  ubthlem2  28299  tpr2rico  30556  xrmulc1cn  30574  omssubadd  30960  sgnmulrp2  31204  ptrecube  34037  poimirlem29  34066  heicant  34072  ftc1anclem6  34117  ftc1anclem7  34118  sstotbnd2  34199  equivtotbnd  34203  totbndbnd  34214  cntotbnd  34221  heibor1lem  34234  heiborlem3  34238  heiborlem6  34241  heiborlem8  34243  supxrge  40466  infrpge  40479  infleinflem1  40498  stoweid  41211  qndenserrnbl  41443  sge0rpcpnf  41566  sge0xaddlem1  41578