Theorem rpxr 13042

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℝ^*cxr 11292  ℝ⁺crp 13032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-un 3968  df-ss 3980  df-xr 11297  df-rp 13033

This theorem is referenced by:  xlemul1  13329  xlemul2  13330  xltmul1  13331  xltmul2  13332  modelico  13918  muladdmodid  13948  sgnrrp  15127  blcntrps  24438  blcntr  24439  blssexps  24452  blssex  24453  blin2  24455  neibl  24530  blnei  24531  metss  24537  metss2lem  24540  stdbdmet  24545  stdbdmopn  24547  metrest  24553  prdsxmslem2  24558  metcnp3  24569  metcnp  24570  metcnpi3  24575  txmetcnp  24576  metustid  24583  cfilucfil  24588  blval2  24591  elbl4  24592  metucn  24600  nmoix  24766  xrsmopn  24848  reperflem  24854  reconnlem2  24863  metdseq0  24890  cnllycmp  25002  lebnum  25010  xlebnum  25011  lebnumii  25012  nmhmcn  25167  lmmbr  25306  lmmbr2  25307  lmnn  25311  cfilfcls  25322  iscau2  25325  iscmet3lem2  25340  equivcfil  25347  flimcfil  25362  cmpcmet  25367  bcthlem5  25376  ellimc3  25929  pige3ALT  26577  efopnlem1  26713  efopnlem2  26714  efopn  26715  xrlimcnp  27026  efrlim  27027  efrlimOLD  27028  lgamcvg2  27113  pntlemi  27663  pntlemp  27669  ubthlem1  30899  xdivpnfrp  32900  pnfinf  33173  signsply0  34545  cnllysconn  35230  poimirlem29  37636  heicant  37642  itg2gt0cn  37662  ftc1anc  37688  areacirclem1  37695  areacirc  37700  blssp  37743  sstotbnd2  37761  isbndx  37769  isbnd2  37770  isbnd3  37771  ssbnd  37775  prdstotbnd  37781  prdsbnd2  37782  cntotbnd  37783  ismtybndlem  37793  heibor1  37797  infleinflem1  45320  limcrecl  45585  islpcn  45595  etransclem18  46208  etransclem46  46236  ioorrnopnlem  46260  sge0iunmptlemre  46371  itscnhlinecirc02p  48635