Theorem rpxr 12968

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝ^*cxr 11214  ℝ⁺crp 12958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-un 3922  df-ss 3934  df-xr 11219  df-rp 12959

This theorem is referenced by:  xlemul1  13257  xlemul2  13258  xltmul1  13259  xltmul2  13260  modelico  13850  muladdmodid  13882  sgnrrp  15064  blcntrps  24307  blcntr  24308  blssexps  24321  blssex  24322  blin2  24324  neibl  24396  blnei  24397  metss  24403  metss2lem  24406  stdbdmet  24411  stdbdmopn  24413  metrest  24419  prdsxmslem2  24424  metcnp3  24435  metcnp  24436  metcnpi3  24441  txmetcnp  24442  metustid  24449  cfilucfil  24454  blval2  24457  elbl4  24458  metucn  24466  nmoix  24624  xrsmopn  24708  reperflem  24714  reconnlem2  24723  metdseq0  24750  cnllycmp  24862  lebnum  24870  xlebnum  24871  lebnumii  24872  nmhmcn  25027  lmmbr  25165  lmmbr2  25166  lmnn  25170  cfilfcls  25181  iscau2  25184  iscmet3lem2  25199  equivcfil  25206  flimcfil  25221  cmpcmet  25226  bcthlem5  25235  ellimc3  25787  pige3ALT  26436  efopnlem1  26572  efopnlem2  26573  efopn  26574  xrlimcnp  26885  efrlim  26886  efrlimOLD  26887  lgamcvg2  26972  pntlemi  27522  pntlemp  27528  ubthlem1  30806  xdivpnfrp  32860  pnfinf  33144  signsply0  34549  cnllysconn  35239  poimirlem29  37650  heicant  37656  itg2gt0cn  37676  ftc1anc  37702  areacirclem1  37709  areacirc  37714  blssp  37757  sstotbnd2  37775  isbndx  37783  isbnd2  37784  isbnd3  37785  ssbnd  37789  prdstotbnd  37795  prdsbnd2  37796  cntotbnd  37797  ismtybndlem  37807  heibor1  37811  infleinflem1  45373  limcrecl  45634  islpcn  45644  etransclem18  46257  etransclem46  46285  ioorrnopnlem  46309  sge0iunmptlemre  46420  itscnhlinecirc02p  48778