Theorem rpxr 12983

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝ^*cxr 11247  ℝ⁺crp 12974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-xr 11252  df-rp 12975

This theorem is referenced by:  xlemul1  13269  xlemul2  13270  xltmul1  13271  xltmul2  13272  modelico  13846  muladdmodid  13876  sgnrrp  15038  blcntrps  23918  blcntr  23919  blssexps  23932  blssex  23933  blin2  23935  neibl  24010  blnei  24011  metss  24017  metss2lem  24020  stdbdmet  24025  stdbdmopn  24027  metrest  24033  prdsxmslem2  24038  metcnp3  24049  metcnp  24050  metcnpi3  24055  txmetcnp  24056  metustid  24063  cfilucfil  24068  blval2  24071  elbl4  24072  metucn  24080  nmoix  24246  xrsmopn  24328  reperflem  24334  reconnlem2  24343  metdseq0  24370  cnllycmp  24472  lebnum  24480  xlebnum  24481  lebnumii  24482  nmhmcn  24636  lmmbr  24775  lmmbr2  24776  lmnn  24780  cfilfcls  24791  iscau2  24794  iscmet3lem2  24809  equivcfil  24816  flimcfil  24831  cmpcmet  24836  bcthlem5  24845  ellimc3  25396  pige3ALT  26029  efopnlem1  26164  efopnlem2  26165  efopn  26166  xrlimcnp  26473  efrlim  26474  lgamcvg2  26559  pntlemi  27107  pntlemp  27113  ubthlem1  30123  xdivpnfrp  32099  pnfinf  32329  signsply0  33562  cnllysconn  34236  poimirlem29  36517  heicant  36523  itg2gt0cn  36543  ftc1anc  36569  areacirclem1  36576  areacirc  36581  blssp  36624  sstotbnd2  36642  isbndx  36650  isbnd2  36651  isbnd3  36652  ssbnd  36656  prdstotbnd  36662  prdsbnd2  36663  cntotbnd  36664  ismtybndlem  36674  heibor1  36678  infleinflem1  44080  limcrecl  44345  islpcn  44355  etransclem18  44968  etransclem46  44996  ioorrnopnlem  45020  sge0iunmptlemre  45131  itscnhlinecirc02p  47471