Theorem rpxr 12668

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝ^*cxr 10939  ℝ⁺crp 12659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-xr 10944  df-rp 12660

This theorem is referenced by:  xlemul1  12953  xlemul2  12954  xltmul1  12955  xltmul2  12956  modelico  13529  muladdmodid  13559  sgnrrp  14730  blcntrps  23473  blcntr  23474  blssexps  23487  blssex  23488  blin2  23490  neibl  23563  blnei  23564  metss  23570  metss2lem  23573  stdbdmet  23578  stdbdmopn  23580  metrest  23586  prdsxmslem2  23591  metcnp3  23602  metcnp  23603  metcnpi3  23608  txmetcnp  23609  metustid  23616  cfilucfil  23621  blval2  23624  elbl4  23625  metucn  23633  nmoix  23799  xrsmopn  23881  reperflem  23887  reconnlem2  23896  metdseq0  23923  cnllycmp  24025  lebnum  24033  xlebnum  24034  lebnumii  24035  nmhmcn  24189  lmmbr  24327  lmmbr2  24328  lmnn  24332  cfilfcls  24343  iscau2  24346  iscmet3lem2  24361  equivcfil  24368  flimcfil  24383  cmpcmet  24388  bcthlem5  24397  ellimc3  24948  pige3ALT  25581  efopnlem1  25716  efopnlem2  25717  efopn  25718  xrlimcnp  26023  efrlim  26024  lgamcvg2  26109  pntlemi  26657  pntlemp  26663  ubthlem1  29133  xdivpnfrp  31109  pnfinf  31339  signsply0  32430  cnllysconn  33107  poimirlem29  35733  heicant  35739  itg2gt0cn  35759  ftc1anc  35785  areacirclem1  35792  areacirc  35797  blssp  35841  sstotbnd2  35859  isbndx  35867  isbnd2  35868  isbnd3  35869  ssbnd  35873  prdstotbnd  35879  prdsbnd2  35880  cntotbnd  35881  ismtybndlem  35891  heibor1  35895  infleinflem1  42799  limcrecl  43060  islpcn  43070  etransclem18  43683  etransclem46  43711  ioorrnopnlem  43735  sge0iunmptlemre  43843  itscnhlinecirc02p  46019