Theorem rpxr 13066

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝ^*cxr 11323  ℝ⁺crp 13057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-un 3981  df-ss 3993  df-xr 11328  df-rp 13058

This theorem is referenced by:  xlemul1  13352  xlemul2  13353  xltmul1  13354  xltmul2  13355  modelico  13932  muladdmodid  13962  sgnrrp  15140  blcntrps  24443  blcntr  24444  blssexps  24457  blssex  24458  blin2  24460  neibl  24535  blnei  24536  metss  24542  metss2lem  24545  stdbdmet  24550  stdbdmopn  24552  metrest  24558  prdsxmslem2  24563  metcnp3  24574  metcnp  24575  metcnpi3  24580  txmetcnp  24581  metustid  24588  cfilucfil  24593  blval2  24596  elbl4  24597  metucn  24605  nmoix  24771  xrsmopn  24853  reperflem  24859  reconnlem2  24868  metdseq0  24895  cnllycmp  25007  lebnum  25015  xlebnum  25016  lebnumii  25017  nmhmcn  25172  lmmbr  25311  lmmbr2  25312  lmnn  25316  cfilfcls  25327  iscau2  25330  iscmet3lem2  25345  equivcfil  25352  flimcfil  25367  cmpcmet  25372  bcthlem5  25381  ellimc3  25934  pige3ALT  26580  efopnlem1  26716  efopnlem2  26717  efopn  26718  xrlimcnp  27029  efrlim  27030  efrlimOLD  27031  lgamcvg2  27116  pntlemi  27666  pntlemp  27672  ubthlem1  30902  xdivpnfrp  32897  pnfinf  33163  signsply0  34528  cnllysconn  35213  poimirlem29  37609  heicant  37615  itg2gt0cn  37635  ftc1anc  37661  areacirclem1  37668  areacirc  37673  blssp  37716  sstotbnd2  37734  isbndx  37742  isbnd2  37743  isbnd3  37744  ssbnd  37748  prdstotbnd  37754  prdsbnd2  37755  cntotbnd  37756  ismtybndlem  37766  heibor1  37770  infleinflem1  45285  limcrecl  45550  islpcn  45560  etransclem18  46173  etransclem46  46201  ioorrnopnlem  46225  sge0iunmptlemre  46336  itscnhlinecirc02p  48519