Theorem rpxr 12943

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝ^*cxr 11169  ℝ⁺crp 12933

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-un 3895  df-ss 3907  df-xr 11174  df-rp 12934

This theorem is referenced by:  xlemul1  13233  xlemul2  13234  xltmul1  13235  xltmul2  13236  modelico  13831  muladdmodid  13863  sgnrrp  15044  blcntrps  24387  blcntr  24388  blssexps  24401  blssex  24402  blin2  24404  neibl  24476  blnei  24477  metss  24483  metss2lem  24486  stdbdmet  24491  stdbdmopn  24493  metrest  24499  prdsxmslem2  24504  metcnp3  24515  metcnp  24516  metcnpi3  24521  txmetcnp  24522  metustid  24529  cfilucfil  24534  blval2  24537  elbl4  24538  metucn  24546  nmoix  24704  xrsmopn  24788  reperflem  24794  reconnlem2  24803  metdseq0  24830  cnllycmp  24933  lebnum  24941  xlebnum  24942  lebnumii  24943  nmhmcn  25097  lmmbr  25235  lmmbr2  25236  lmnn  25240  cfilfcls  25251  iscau2  25254  iscmet3lem2  25269  equivcfil  25276  flimcfil  25291  cmpcmet  25296  bcthlem5  25305  ellimc3  25856  pige3ALT  26497  efopnlem1  26633  efopnlem2  26634  efopn  26635  xrlimcnp  26945  efrlim  26946  efrlimOLD  26947  lgamcvg2  27032  pntlemi  27581  pntlemp  27587  ubthlem1  30956  xdivpnfrp  33007  pnfinf  33259  signsply0  34711  cnllysconn  35443  poimirlem29  37984  heicant  37990  itg2gt0cn  38010  ftc1anc  38036  areacirclem1  38043  areacirc  38048  blssp  38091  sstotbnd2  38109  isbndx  38117  isbnd2  38118  isbnd3  38119  ssbnd  38123  prdstotbnd  38129  prdsbnd2  38130  cntotbnd  38131  ismtybndlem  38141  heibor1  38145  infleinflem1  45817  limcrecl  46077  islpcn  46085  etransclem18  46698  etransclem46  46726  ioorrnopnlem  46750  sge0iunmptlemre  46861  itscnhlinecirc02p  49273