Theorem rpxr 13017

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 13016	. 2 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)
2	1	rexrd 11247	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ*)

Syntax hints:   → wi 4   ∈ wcel 2145  ℝ^*cxr 11230  ℝ⁺crp 13007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-un 3912  df-ss 3924  df-xr 11235  df-rp 13008

This theorem is referenced by:  xlemul1  13307  xlemul2  13308  xltmul1  13309  xltmul2  13310  modelico  13905  muladdmodid  13937  sgnrrp  15118  blcntrps  24530  blcntr  24531  blssexps  24544  blssex  24545  blin2  24547  neibl  24619  blnei  24620  metss  24626  metss2lem  24629  stdbdmet  24634  stdbdmopn  24636  metrest  24642  prdsxmslem2  24647  metcnp3  24658  metcnp  24659  metcnpi3  24664  txmetcnp  24665  metustid  24672  cfilucfil  24677  blval2  24680  elbl4  24681  metucn  24689  nmoix  24847  xrsmopn  24931  reperflem  24937  reconnlem2  24946  metdseq0  24973  cnllycmp  25076  lebnum  25084  xlebnum  25085  lebnumii  25086  nmhmcn  25240  lmmbr  25378  lmmbr2  25379  lmnn  25383  cfilfcls  25394  iscau2  25397  iscmet3lem2  25412  equivcfil  25419  flimcfil  25434  cmpcmet  25439  bcthlem5  25448  ellimc3  25999  pige3ALT  26643  efopnlem1  26779  efopnlem2  26780  efopn  26781  xrlimcnp  27091  efrlim  27092  lgamcvg2  27177  pntlemi  27726  pntlemp  27732  ubthlem1  31131  xdivpnfrp  33165  pnfinf  33416  signsply0  34855  cnllysconn  35608  poimirlem29  38160  heicant  38166  itg2gt0cn  38186  ftc1anc  38212  areacirclem1  38219  areacirc  38224  blssp  38267  sstotbnd2  38285  isbndx  38293  isbnd2  38294  isbnd3  38295  ssbnd  38299  prdstotbnd  38305  prdsbnd2  38306  cntotbnd  38307  ismtybndlem  38317  heibor1  38321  infleinflem1  45943  limcrecl  46203  islpcn  46211  etransclem18  46824  etransclem46  46852  ioorrnopnlem  46876  sge0iunmptlemre  46987  itscnhlinecirc02p  49416