Theorem rpxr 12979

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

Syntax hints:   → wi 4   ∈ wcel 2098  ℝ^*cxr 11243  ℝ⁺crp 12970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-un 3945  df-in 3947  df-ss 3957  df-xr 11248  df-rp 12971

This theorem is referenced by:  xlemul1  13265  xlemul2  13266  xltmul1  13267  xltmul2  13268  modelico  13842  muladdmodid  13872  sgnrrp  15034  blcntrps  24228  blcntr  24229  blssexps  24242  blssex  24243  blin2  24245  neibl  24320  blnei  24321  metss  24327  metss2lem  24330  stdbdmet  24335  stdbdmopn  24337  metrest  24343  prdsxmslem2  24348  metcnp3  24359  metcnp  24360  metcnpi3  24365  txmetcnp  24366  metustid  24373  cfilucfil  24378  blval2  24381  elbl4  24382  metucn  24390  nmoix  24556  xrsmopn  24638  reperflem  24644  reconnlem2  24653  metdseq0  24680  cnllycmp  24792  lebnum  24800  xlebnum  24801  lebnumii  24802  nmhmcn  24957  lmmbr  25096  lmmbr2  25097  lmnn  25101  cfilfcls  25112  iscau2  25115  iscmet3lem2  25130  equivcfil  25137  flimcfil  25152  cmpcmet  25157  bcthlem5  25166  ellimc3  25718  pige3ALT  26359  efopnlem1  26494  efopnlem2  26495  efopn  26496  xrlimcnp  26804  efrlim  26805  efrlimOLD  26806  lgamcvg2  26891  pntlemi  27441  pntlemp  27447  ubthlem1  30547  xdivpnfrp  32523  pnfinf  32756  signsply0  34017  cnllysconn  34691  poimirlem29  36973  heicant  36979  itg2gt0cn  36999  ftc1anc  37025  areacirclem1  37032  areacirc  37037  blssp  37080  sstotbnd2  37098  isbndx  37106  isbnd2  37107  isbnd3  37108  ssbnd  37112  prdstotbnd  37118  prdsbnd2  37119  cntotbnd  37120  ismtybndlem  37130  heibor1  37134  infleinflem1  44531  limcrecl  44796  islpcn  44806  etransclem18  45419  etransclem46  45447  ioorrnopnlem  45471  sge0iunmptlemre  45582  itscnhlinecirc02p  47625