Theorem rpxr 12933

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℝ^*cxr 11197  ℝ⁺crp 12924

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-un 3918  df-in 3920  df-ss 3930  df-xr 11202  df-rp 12925

This theorem is referenced by:  xlemul1  13219  xlemul2  13220  xltmul1  13221  xltmul2  13222  modelico  13796  muladdmodid  13826  sgnrrp  14988  blcntrps  23802  blcntr  23803  blssexps  23816  blssex  23817  blin2  23819  neibl  23894  blnei  23895  metss  23901  metss2lem  23904  stdbdmet  23909  stdbdmopn  23911  metrest  23917  prdsxmslem2  23922  metcnp3  23933  metcnp  23934  metcnpi3  23939  txmetcnp  23940  metustid  23947  cfilucfil  23952  blval2  23955  elbl4  23956  metucn  23964  nmoix  24130  xrsmopn  24212  reperflem  24218  reconnlem2  24227  metdseq0  24254  cnllycmp  24356  lebnum  24364  xlebnum  24365  lebnumii  24366  nmhmcn  24520  lmmbr  24659  lmmbr2  24660  lmnn  24664  cfilfcls  24675  iscau2  24678  iscmet3lem2  24693  equivcfil  24700  flimcfil  24715  cmpcmet  24720  bcthlem5  24729  ellimc3  25280  pige3ALT  25913  efopnlem1  26048  efopnlem2  26049  efopn  26050  xrlimcnp  26355  efrlim  26356  lgamcvg2  26441  pntlemi  26989  pntlemp  26995  ubthlem1  29875  xdivpnfrp  31859  pnfinf  32089  signsply0  33252  cnllysconn  33926  poimirlem29  36180  heicant  36186  itg2gt0cn  36206  ftc1anc  36232  areacirclem1  36239  areacirc  36244  blssp  36288  sstotbnd2  36306  isbndx  36314  isbnd2  36315  isbnd3  36316  ssbnd  36320  prdstotbnd  36326  prdsbnd2  36327  cntotbnd  36328  ismtybndlem  36338  heibor1  36342  infleinflem1  43725  limcrecl  43990  islpcn  44000  etransclem18  44613  etransclem46  44641  ioorrnopnlem  44665  sge0iunmptlemre  44776  itscnhlinecirc02p  46991