Theorem rpxr 13133

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℝ^*cxr 11345  ℝ⁺crp 13123

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-un 4151  df-xr 11350  df-rp 13124

This theorem is used by:  xlemul1  13423  xlemul2  13424  xltmul1  13425  xltmul2  13426  modelico  14024  muladdmodid  14056  sgnrrp  15249  blcntrps  24736  blcntr  24737  blssexps  24750  blssex  24751  blin2  24753  neibl  24825  blnei  24826  metss  24832  metss2lem  24835  stdbdmet  24840  stdbdmopn  24842  metrest  24848  prdsxmslem2  24853  metcnp3  24864  metcnp  24865  metcnpi3  24870  txmetcnp  24871  metustid  24878  cfilucfil  24883  blval2  24886  elbl4  24887  metucn  24895  nmoix  25053  xrsmopn  25137  reperflem  25143  reconnlem2  25152  metdseq0  25179  cnllycmp  25282  lebnum  25290  xlebnum  25291  lebnumii  25292  nmhmcn  25446  lmmbr  25584  lmmbr2  25585  lmnn  25589  cfilfcls  25600  iscau2  25603  iscmet3lem2  25618  equivcfil  25625  flimcfil  25640  cmpcmet  25645  bcthlem5  25654  ellimc3  26204  pige3ALT  26853  efopnlem1  26989  efopnlem2  26990  efopn  26991  xrlimcnp  27301  efrlim  27302  lgamcvg2  27387  pntlemi  27936  pntlemp  27942  ubthlem1  31477  xdivpnfrp  33545  pnfinf  33790  signsply0  35226  cnllysconn  36096  poimirlem29  38660  heicant  38666  itg2gt0cn  38686  ftc1anc  38712  areacirclem1  38719  areacirc  38724  blssp  38783  sstotbnd2  38801  isbndx  38809  isbnd2  38810  isbnd3  38811  ssbnd  38815  prdstotbnd  38821  prdsbnd2  38822  cntotbnd  38823  ismtybndlem  38833  heibor1  38837  infleinflem1  46474  limcrecl  46734  islpcn  46742  etransclem18  47355  etransclem46  47383  ioorrnopnlem  47407  sge0iunmptlemre  47518  itscnhlinecirc02p  49990