Theorem rpxr 12739

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℝ^*cxr 11008  ℝ⁺crp 12730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-xr 11013  df-rp 12731

This theorem is referenced by:  xlemul1  13024  xlemul2  13025  xltmul1  13026  xltmul2  13027  modelico  13601  muladdmodid  13631  sgnrrp  14802  blcntrps  23565  blcntr  23566  blssexps  23579  blssex  23580  blin2  23582  neibl  23657  blnei  23658  metss  23664  metss2lem  23667  stdbdmet  23672  stdbdmopn  23674  metrest  23680  prdsxmslem2  23685  metcnp3  23696  metcnp  23697  metcnpi3  23702  txmetcnp  23703  metustid  23710  cfilucfil  23715  blval2  23718  elbl4  23719  metucn  23727  nmoix  23893  xrsmopn  23975  reperflem  23981  reconnlem2  23990  metdseq0  24017  cnllycmp  24119  lebnum  24127  xlebnum  24128  lebnumii  24129  nmhmcn  24283  lmmbr  24422  lmmbr2  24423  lmnn  24427  cfilfcls  24438  iscau2  24441  iscmet3lem2  24456  equivcfil  24463  flimcfil  24478  cmpcmet  24483  bcthlem5  24492  ellimc3  25043  pige3ALT  25676  efopnlem1  25811  efopnlem2  25812  efopn  25813  xrlimcnp  26118  efrlim  26119  lgamcvg2  26204  pntlemi  26752  pntlemp  26758  ubthlem1  29232  xdivpnfrp  31207  pnfinf  31437  signsply0  32530  cnllysconn  33207  poimirlem29  35806  heicant  35812  itg2gt0cn  35832  ftc1anc  35858  areacirclem1  35865  areacirc  35870  blssp  35914  sstotbnd2  35932  isbndx  35940  isbnd2  35941  isbnd3  35942  ssbnd  35946  prdstotbnd  35952  prdsbnd2  35953  cntotbnd  35954  ismtybndlem  35964  heibor1  35968  infleinflem1  42909  limcrecl  43170  islpcn  43180  etransclem18  43793  etransclem46  43821  ioorrnopnlem  43845  sge0iunmptlemre  43953  itscnhlinecirc02p  46131