Theorem rpxr 13157

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℝ^*cxr 11369  ℝ⁺crp 13147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-un 4154  df-xr 11374  df-rp 13148

This theorem is used by:  xlemul1  13447  xlemul2  13448  xltmul1  13449  xltmul2  13450  modelico  14048  muladdmodid  14080  sgnrrp  15273  blcntrps  24761  blcntr  24762  blssexps  24775  blssex  24776  blin2  24778  neibl  24850  blnei  24851  metss  24857  metss2lem  24860  stdbdmet  24865  stdbdmopn  24867  metrest  24873  prdsxmslem2  24878  metcnp3  24889  metcnp  24890  metcnpi3  24895  txmetcnp  24896  metustid  24903  cfilucfil  24908  blval2  24911  elbl4  24912  metucn  24920  nmoix  25078  xrsmopn  25162  reperflem  25168  reconnlem2  25177  metdseq0  25204  cnllycmp  25307  lebnum  25315  xlebnum  25316  lebnumii  25317  nmhmcn  25471  lmmbr  25609  lmmbr2  25610  lmnn  25614  cfilfcls  25625  iscau2  25628  iscmet3lem2  25643  equivcfil  25650  flimcfil  25665  cmpcmet  25670  bcthlem5  25679  ellimc3  26229  pige3ALT  26878  efopnlem1  27014  efopnlem2  27015  efopn  27016  xrlimcnp  27326  efrlim  27327  lgamcvg2  27412  pntlemi  27961  pntlemp  27967  ubthlem1  31502  xdivpnfrp  33569  pnfinf  33814  signsply0  35250  cnllysconn  36177  poimirlem29  38759  heicant  38765  itg2gt0cn  38785  ftc1anc  38811  areacirclem1  38818  areacirc  38823  blssp  38882  sstotbnd2  38900  isbndx  38908  isbnd2  38909  isbnd3  38910  ssbnd  38914  prdstotbnd  38920  prdsbnd2  38921  cntotbnd  38922  ismtybndlem  38932  heibor1  38936  infleinflem1  46586  limcrecl  46846  islpcn  46854  etransclem18  47467  etransclem46  47495  ioorrnopnlem  47519  sge0iunmptlemre  47630  itscnhlinecirc02p  50102