Theorem rpxr 12952

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝ^*cxr 11178  ℝ⁺crp 12942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-un 3894  df-ss 3906  df-xr 11183  df-rp 12943

This theorem is referenced by:  xlemul1  13242  xlemul2  13243  xltmul1  13244  xltmul2  13245  modelico  13840  muladdmodid  13872  sgnrrp  15053  blcntrps  24377  blcntr  24378  blssexps  24391  blssex  24392  blin2  24394  neibl  24466  blnei  24467  metss  24473  metss2lem  24476  stdbdmet  24481  stdbdmopn  24483  metrest  24489  prdsxmslem2  24494  metcnp3  24505  metcnp  24506  metcnpi3  24511  txmetcnp  24512  metustid  24519  cfilucfil  24524  blval2  24527  elbl4  24528  metucn  24536  nmoix  24694  xrsmopn  24778  reperflem  24784  reconnlem2  24793  metdseq0  24820  cnllycmp  24923  lebnum  24931  xlebnum  24932  lebnumii  24933  nmhmcn  25087  lmmbr  25225  lmmbr2  25226  lmnn  25230  cfilfcls  25241  iscau2  25244  iscmet3lem2  25259  equivcfil  25266  flimcfil  25281  cmpcmet  25286  bcthlem5  25295  ellimc3  25846  pige3ALT  26484  efopnlem1  26620  efopnlem2  26621  efopn  26622  xrlimcnp  26932  efrlim  26933  lgamcvg2  27018  pntlemi  27567  pntlemp  27573  ubthlem1  30941  xdivpnfrp  32992  pnfinf  33244  signsply0  34695  cnllysconn  35427  poimirlem29  37970  heicant  37976  itg2gt0cn  37996  ftc1anc  38022  areacirclem1  38029  areacirc  38034  blssp  38077  sstotbnd2  38095  isbndx  38103  isbnd2  38104  isbnd3  38105  ssbnd  38109  prdstotbnd  38115  prdsbnd2  38116  cntotbnd  38117  ismtybndlem  38127  heibor1  38131  infleinflem1  45799  limcrecl  46059  islpcn  46067  etransclem18  46680  etransclem46  46708  ioorrnopnlem  46732  sge0iunmptlemre  46843  itscnhlinecirc02p  49261