Theorem rpxrd 12515

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝ^*cxr 10752  ℝ⁺crp 12472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-rab 3062  df-v 3400  df-un 3848  df-in 3850  df-ss 3860  df-xr 10757  df-rp 12473

This theorem is referenced by:  ssblex  23181  metequiv2  23263  metss2lem  23264  methaus  23273  met1stc  23274  met2ndci  23275  metcnp  23294  metcnpi3  23299  metustexhalf  23309  blval2  23315  metuel2  23318  nmoi2  23483  metdcnlem  23588  metdscnlem  23607  metnrmlem2  23612  metnrmlem3  23613  cnheibor  23707  cnllycmp  23708  lebnumlem3  23715  nmoleub2lem  23866  nmhmcn  23872  iscfil2  24018  cfil3i  24021  iscfil3  24025  cfilfcls  24026  iscmet3lem2  24044  caubl  24060  caublcls  24061  relcmpcmet  24070  bcthlem2  24077  bcthlem4  24079  bcthlem5  24080  ellimc3  24631  ftc1a  24789  ulmdvlem1  25147  psercnlem2  25171  psercn  25173  pserdvlem2  25175  pserdv  25176  efopn  25401  logccv  25406  efrlim  25707  lgamucov  25775  ftalem3  25812  logexprlim  25961  pntpbnd1a  26321  pntleme  26344  pntlem3  26345  pntleml  26347  ubthlem1  28805  ubthlem2  28806  tpr2rico  31434  xrmulc1cn  31452  omssubadd  31837  sgnmulrp2  32080  ptrecube  35400  poimirlem29  35429  heicant  35435  ftc1anclem6  35478  ftc1anclem7  35479  sstotbnd2  35555  equivtotbnd  35559  totbndbnd  35570  cntotbnd  35577  heibor1lem  35590  heiborlem3  35594  heiborlem6  35597  heiborlem8  35599  supxrge  42415  infrpge  42428  infleinflem1  42447  stoweid  43146  qndenserrnbl  43378  sge0rpcpnf  43501  sge0xaddlem1  43513