Theorem rpxr 13056

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝ^*cxr 11270  ℝ⁺crp 13046

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-un 3907  df-ss 3919  df-xr 11275  df-rp 13047

This theorem is used by:  xlemul1  13346  xlemul2  13347  xltmul1  13348  xltmul2  13349  modelico  13946  muladdmodid  13978  sgnrrp  15168  blcntrps  24644  blcntr  24645  blssexps  24658  blssex  24659  blin2  24661  neibl  24733  blnei  24734  metss  24740  metss2lem  24743  stdbdmet  24748  stdbdmopn  24750  metrest  24756  prdsxmslem2  24761  metcnp3  24772  metcnp  24773  metcnpi3  24778  txmetcnp  24779  metustid  24786  cfilucfil  24791  blval2  24794  elbl4  24795  metucn  24803  nmoix  24961  xrsmopn  25045  reperflem  25051  reconnlem2  25060  metdseq0  25087  cnllycmp  25190  lebnum  25198  xlebnum  25199  lebnumii  25200  nmhmcn  25354  lmmbr  25492  lmmbr2  25493  lmnn  25497  cfilfcls  25508  iscau2  25511  iscmet3lem2  25526  equivcfil  25533  flimcfil  25548  cmpcmet  25553  bcthlem5  25562  ellimc3  26113  pige3ALT  26765  efopnlem1  26901  efopnlem2  26902  efopn  26903  xrlimcnp  27213  efrlim  27214  lgamcvg2  27299  pntlemi  27848  pntlemp  27854  ubthlem1  31359  xdivpnfrp  33386  pnfinf  33631  signsply0  35067  cnllysconn  35832  poimirlem29  38406  heicant  38412  itg2gt0cn  38432  ftc1anc  38458  areacirclem1  38465  areacirc  38470  blssp  38514  sstotbnd2  38532  isbndx  38540  isbnd2  38541  isbnd3  38542  ssbnd  38546  prdstotbnd  38552  prdsbnd2  38553  cntotbnd  38554  ismtybndlem  38564  heibor1  38568  infleinflem1  46207  limcrecl  46467  islpcn  46475  etransclem18  47088  etransclem46  47116  ioorrnopnlem  47140  sge0iunmptlemre  47251  itscnhlinecirc02p  49723