Theorem rpxr 13111

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝ^*cxr 11323  ℝ⁺crp 13101

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904  df-ss 3916  df-xr 11328  df-rp 13102

This theorem is used by:  xlemul1  13401  xlemul2  13402  xltmul1  13403  xltmul2  13404  modelico  14001  muladdmodid  14033  sgnrrp  15224  blcntrps  24711  blcntr  24712  blssexps  24725  blssex  24726  blin2  24728  neibl  24800  blnei  24801  metss  24807  metss2lem  24810  stdbdmet  24815  stdbdmopn  24817  metrest  24823  prdsxmslem2  24828  metcnp3  24839  metcnp  24840  metcnpi3  24845  txmetcnp  24846  metustid  24853  cfilucfil  24858  blval2  24861  elbl4  24862  metucn  24870  nmoix  25028  xrsmopn  25112  reperflem  25118  reconnlem2  25127  metdseq0  25154  cnllycmp  25257  lebnum  25265  xlebnum  25266  lebnumii  25267  nmhmcn  25421  lmmbr  25559  lmmbr2  25560  lmnn  25564  cfilfcls  25575  iscau2  25578  iscmet3lem2  25593  equivcfil  25600  flimcfil  25615  cmpcmet  25620  bcthlem5  25629  ellimc3  26179  pige3ALT  26830  efopnlem1  26966  efopnlem2  26967  efopn  26968  xrlimcnp  27278  efrlim  27279  lgamcvg2  27364  pntlemi  27913  pntlemp  27919  ubthlem1  31454  xdivpnfrp  33481  pnfinf  33726  signsply0  35163  cnllysconn  35979  poimirlem29  38535  heicant  38541  itg2gt0cn  38561  ftc1anc  38587  areacirclem1  38594  areacirc  38599  blssp  38658  sstotbnd2  38676  isbndx  38684  isbnd2  38685  isbnd3  38686  ssbnd  38690  prdstotbnd  38696  prdsbnd2  38697  cntotbnd  38698  ismtybndlem  38708  heibor1  38712  infleinflem1  46325  limcrecl  46585  islpcn  46593  etransclem18  47206  etransclem46  47234  ioorrnopnlem  47258  sge0iunmptlemre  47369  itscnhlinecirc02p  49841