Theorem rpxrd 11749

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℝ^*cxr 9952  ℝ⁺crp 11708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-xr 9957  df-rp 11709

This theorem is referenced by:  ssblex  22043  metequiv2  22125  metss2lem  22126  methaus  22135  met1stc  22136  met2ndci  22137  metcnp  22156  metcnpi3  22161  metustexhalf  22171  blval2  22177  metuel2  22180  nmoi2  22344  metdcnlem  22447  metdscnlem  22466  metnrmlem2  22471  metnrmlem3  22472  cnheibor  22562  cnllycmp  22563  lebnumlem3  22570  nmoleub2lem  22722  nmhmcn  22728  iscfil2  22872  cfil3i  22875  iscfil3  22879  iscmet3lem2  22898  caubl  22914  caublcls  22915  relcmpcmet  22923  bcthlem2  22930  bcthlem4  22932  bcthlem5  22933  ellimc3  23449  ftc1a  23604  ulmdvlem1  23958  psercnlem2  23982  psercn  23984  pserdvlem2  23986  pserdv  23987  efopn  24204  logccv  24209  efrlim  24496  lgamucov  24564  ftalem3  24601  logexprlim  24750  pntpbnd1a  25074  pntleme  25097  pntlem3  25098  pntleml  25100  ubthlem1  27110  ubthlem2  27111  tpr2rico  29286  xrmulc1cn  29304  omssubadd  29689  sgnmulrp2  29932  ptrecube  32579  poimirlem29  32608  heicant  32614  ftc1anclem6  32660  ftc1anclem7  32661  sstotbnd2  32743  equivtotbnd  32747  totbndbnd  32758  cntotbnd  32765  heibor1lem  32778  heiborlem3  32782  heiborlem6  32785  heiborlem8  32787  supxrge  38495  infrpge  38508  infleinflem1  38527  stoweid  38956  qndenserrnbl  39191  sge0rpcpnf  39314  sge0xaddlem1  39326