Theorem rpxr 12921

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝ^*cxr 11167  ℝ⁺crp 12911

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-un 3910  df-ss 3922  df-xr 11172  df-rp 12912

This theorem is referenced by:  xlemul1  13210  xlemul2  13211  xltmul1  13212  xltmul2  13213  modelico  13803  muladdmodid  13835  sgnrrp  15016  blcntrps  24316  blcntr  24317  blssexps  24330  blssex  24331  blin2  24333  neibl  24405  blnei  24406  metss  24412  metss2lem  24415  stdbdmet  24420  stdbdmopn  24422  metrest  24428  prdsxmslem2  24433  metcnp3  24444  metcnp  24445  metcnpi3  24450  txmetcnp  24451  metustid  24458  cfilucfil  24463  blval2  24466  elbl4  24467  metucn  24475  nmoix  24633  xrsmopn  24717  reperflem  24723  reconnlem2  24732  metdseq0  24759  cnllycmp  24871  lebnum  24879  xlebnum  24880  lebnumii  24881  nmhmcn  25036  lmmbr  25174  lmmbr2  25175  lmnn  25179  cfilfcls  25190  iscau2  25193  iscmet3lem2  25208  equivcfil  25215  flimcfil  25230  cmpcmet  25235  bcthlem5  25244  ellimc3  25796  pige3ALT  26445  efopnlem1  26581  efopnlem2  26582  efopn  26583  xrlimcnp  26894  efrlim  26895  efrlimOLD  26896  lgamcvg2  26981  pntlemi  27531  pntlemp  27537  ubthlem1  30832  xdivpnfrp  32886  pnfinf  33135  signsply0  34518  cnllysconn  35217  poimirlem29  37628  heicant  37634  itg2gt0cn  37654  ftc1anc  37680  areacirclem1  37687  areacirc  37692  blssp  37735  sstotbnd2  37753  isbndx  37761  isbnd2  37762  isbnd3  37763  ssbnd  37767  prdstotbnd  37773  prdsbnd2  37774  cntotbnd  37775  ismtybndlem  37785  heibor1  37789  infleinflem1  45350  limcrecl  45611  islpcn  45621  etransclem18  46234  etransclem46  46262  ioorrnopnlem  46286  sge0iunmptlemre  46397  itscnhlinecirc02p  48771