Theorem rpxr 12897

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝ^*cxr 11142  ℝ⁺crp 12887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-un 3907  df-ss 3919  df-xr 11147  df-rp 12888

This theorem is referenced by:  xlemul1  13186  xlemul2  13187  xltmul1  13188  xltmul2  13189  modelico  13782  muladdmodid  13814  sgnrrp  14995  blcntrps  24325  blcntr  24326  blssexps  24339  blssex  24340  blin2  24342  neibl  24414  blnei  24415  metss  24421  metss2lem  24424  stdbdmet  24429  stdbdmopn  24431  metrest  24437  prdsxmslem2  24442  metcnp3  24453  metcnp  24454  metcnpi3  24459  txmetcnp  24460  metustid  24467  cfilucfil  24472  blval2  24475  elbl4  24476  metucn  24484  nmoix  24642  xrsmopn  24726  reperflem  24732  reconnlem2  24741  metdseq0  24768  cnllycmp  24880  lebnum  24888  xlebnum  24889  lebnumii  24890  nmhmcn  25045  lmmbr  25183  lmmbr2  25184  lmnn  25188  cfilfcls  25199  iscau2  25202  iscmet3lem2  25217  equivcfil  25224  flimcfil  25239  cmpcmet  25244  bcthlem5  25253  ellimc3  25805  pige3ALT  26454  efopnlem1  26590  efopnlem2  26591  efopn  26592  xrlimcnp  26903  efrlim  26904  efrlimOLD  26905  lgamcvg2  26990  pntlemi  27540  pntlemp  27546  ubthlem1  30845  xdivpnfrp  32908  pnfinf  33147  signsply0  34559  cnllysconn  35277  poimirlem29  37688  heicant  37694  itg2gt0cn  37714  ftc1anc  37740  areacirclem1  37747  areacirc  37752  blssp  37795  sstotbnd2  37813  isbndx  37821  isbnd2  37822  isbnd3  37823  ssbnd  37827  prdstotbnd  37833  prdsbnd2  37834  cntotbnd  37835  ismtybndlem  37845  heibor1  37849  infleinflem1  45407  limcrecl  45668  islpcn  45676  etransclem18  46289  etransclem46  46317  ioorrnopnlem  46341  sge0iunmptlemre  46452  itscnhlinecirc02p  48816