Theorem rpxrd 12981

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝ^*cxr 11172  ℝ⁺crp 12936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-un 3895  df-ss 3907  df-xr 11177  df-rp 12937

This theorem is referenced by:  ssblex  24406  metequiv2  24488  metss2lem  24489  methaus  24498  met1stc  24499  met2ndci  24500  metcnp  24519  metcnpi3  24524  metustexhalf  24534  blval2  24540  metuel2  24543  nmoi2  24708  metdcnlem  24815  metdscnlem  24834  metnrmlem2  24839  metnrmlem3  24840  cnheibor  24935  cnllycmp  24936  lebnumlem3  24943  nmoleub2lem  25094  nmhmcn  25100  iscfil2  25246  cfil3i  25249  iscfil3  25253  cfilfcls  25254  iscmet3lem2  25272  caubl  25288  caublcls  25289  relcmpcmet  25298  bcthlem2  25305  bcthlem4  25307  bcthlem5  25308  ellimc3  25859  ftc1a  26017  ulmdvlem1  26381  psercnlem2  26405  psercn  26407  pserdvlem2  26409  pserdv  26410  efopn  26638  logccv  26643  efrlim  26949  efrlimOLD  26950  lgamucov  27018  ftalem3  27055  logexprlim  27205  pntpbnd1a  27565  pntleme  27588  pntlem3  27589  pntleml  27591  ubthlem1  30959  ubthlem2  30960  sgnmulrp2  32927  tpr2rico  34075  xrmulc1cn  34093  omssubadd  34463  ptrecube  37958  poimirlem29  37987  heicant  37993  ftc1anclem6  38036  ftc1anclem7  38037  sstotbnd2  38112  equivtotbnd  38116  totbndbnd  38127  cntotbnd  38134  heibor1lem  38147  heiborlem3  38151  heiborlem6  38154  heiborlem8  38156  supxrge  45789  infrpge  45802  infleinflem1  45820  stoweid  46512  qndenserrnbl  46744  sge0rpcpnf  46870  sge0xaddlem1  46882