Theorem rpxrd 13056

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℝ^*cxr 11237  ℝ⁺crp 13011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-un 3910  df-ss 3922  df-xr 11242  df-rp 13012

This theorem is referenced by:  sgnmulrp2  15141  ssblex  24585  metequiv2  24667  metss2lem  24668  methaus  24677  met1stc  24678  met2ndci  24679  metcnp  24698  metcnpi3  24703  metustexhalf  24713  blval2  24719  metuel2  24722  nmoi2  24887  metdcnlem  24994  metdscnlem  25013  metnrmlem2  25018  metnrmlem3  25019  cnheibor  25114  cnllycmp  25115  lebnumlem3  25122  nmoleub2lem  25273  nmhmcn  25279  iscfil2  25425  cfil3i  25428  iscfil3  25432  cfilfcls  25433  iscmet3lem2  25451  caubl  25467  caublcls  25468  relcmpcmet  25477  bcthlem2  25484  bcthlem4  25486  bcthlem5  25487  ellimc3  26038  ftc1a  26196  ulmdvlem1  26563  psercnlem2  26587  psercn  26589  pserdvlem2  26591  pserdv  26592  efopn  26823  logccv  26828  efrlim  27134  lgamucov  27202  ftalem3  27239  logexprlim  27389  pntpbnd1a  27749  pntleme  27772  pntlem3  27773  pntleml  27775  ubthlem1  31222  ubthlem2  31223  tpr2rico  34302  xrmulc1cn  34320  omssubadd  34690  ptrecube  38271  poimirlem29  38300  heicant  38306  ftc1anclem6  38349  ftc1anclem7  38350  sstotbnd2  38425  equivtotbnd  38429  totbndbnd  38440  cntotbnd  38447  heibor1lem  38460  heiborlem3  38464  heiborlem6  38467  heiborlem8  38469  supxrge  46054  infrpge  46067  infleinflem1  46085  stoweid  46777  qndenserrnbl  47009  sge0rpcpnf  47135  sge0xaddlem1  47147