Theorem rpxr 12927

Description: A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.)

Assertion

Ref	Expression
rpxr	⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*)

Proof of Theorem rpxr

Step	Hyp	Ref	Expression
1		rpre 12926	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
2	1	rexrd 11194	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2114  ℝ^*cxr 11177  ℝ⁺crp 12917

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 3402  df-v 3444  df-un 3908  df-ss 3920  df-xr 11182  df-rp 12918

This theorem is referenced by:  xlemul1  13217  xlemul2  13218  xltmul1  13219  xltmul2  13220  modelico  13813  muladdmodid  13845  sgnrrp  15026  blcntrps  24368  blcntr  24369  blssexps  24382  blssex  24383  blin2  24385  neibl  24457  blnei  24458  metss  24464  metss2lem  24467  stdbdmet  24472  stdbdmopn  24474  metrest  24480  prdsxmslem2  24485  metcnp3  24496  metcnp  24497  metcnpi3  24502  txmetcnp  24503  metustid  24510  cfilucfil  24515  blval2  24518  elbl4  24519  metucn  24527  nmoix  24685  xrsmopn  24769  reperflem  24775  reconnlem2  24784  metdseq0  24811  cnllycmp  24923  lebnum  24931  xlebnum  24932  lebnumii  24933  nmhmcn  25088  lmmbr  25226  lmmbr2  25227  lmnn  25231  cfilfcls  25242  iscau2  25245  iscmet3lem2  25260  equivcfil  25267  flimcfil  25282  cmpcmet  25287  bcthlem5  25296  ellimc3  25848  pige3ALT  26497  efopnlem1  26633  efopnlem2  26634  efopn  26635  xrlimcnp  26946  efrlim  26947  efrlimOLD  26948  lgamcvg2  27033  pntlemi  27583  pntlemp  27589  ubthlem1  30957  xdivpnfrp  33024  pnfinf  33276  signsply0  34728  cnllysconn  35458  poimirlem29  37894  heicant  37900  itg2gt0cn  37920  ftc1anc  37946  areacirclem1  37953  areacirc  37958  blssp  38001  sstotbnd2  38019  isbndx  38027  isbnd2  38028  isbnd3  38029  ssbnd  38033  prdstotbnd  38039  prdsbnd2  38040  cntotbnd  38041  ismtybndlem  38051  heibor1  38055  infleinflem1  45722  limcrecl  45983  islpcn  45991  etransclem18  46604  etransclem46  46632  ioorrnopnlem  46656  sge0iunmptlemre  46767  itscnhlinecirc02p  49139