Theorem rpxr 13044

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℝ^*cxr 11260  ℝ⁺crp 13034

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-un 3913  df-ss 3925  df-xr 11265  df-rp 13035

This theorem is used by:  xlemul1  13334  xlemul2  13335  xltmul1  13336  xltmul2  13337  modelico  13934  muladdmodid  13966  sgnrrp  15154  blcntrps  24606  blcntr  24607  blssexps  24620  blssex  24621  blin2  24623  neibl  24695  blnei  24696  metss  24702  metss2lem  24705  stdbdmet  24710  stdbdmopn  24712  metrest  24718  prdsxmslem2  24723  metcnp3  24734  metcnp  24735  metcnpi3  24740  txmetcnp  24741  metustid  24748  cfilucfil  24753  blval2  24756  elbl4  24757  metucn  24765  nmoix  24923  xrsmopn  25007  reperflem  25013  reconnlem2  25022  metdseq0  25049  cnllycmp  25152  lebnum  25160  xlebnum  25161  lebnumii  25162  nmhmcn  25316  lmmbr  25454  lmmbr2  25455  lmnn  25459  cfilfcls  25470  iscau2  25473  iscmet3lem2  25488  equivcfil  25495  flimcfil  25510  cmpcmet  25515  bcthlem5  25524  ellimc3  26075  pige3ALT  26722  efopnlem1  26858  efopnlem2  26859  efopn  26860  xrlimcnp  27170  efrlim  27171  lgamcvg2  27256  pntlemi  27805  pntlemp  27811  ubthlem1  31259  xdivpnfrp  33289  pnfinf  33534  signsply0  34970  cnllysconn  35758  poimirlem29  38341  heicant  38347  itg2gt0cn  38367  ftc1anc  38393  areacirclem1  38400  areacirc  38405  blssp  38448  sstotbnd2  38466  isbndx  38474  isbnd2  38475  isbnd3  38476  ssbnd  38480  prdstotbnd  38486  prdsbnd2  38487  cntotbnd  38488  ismtybndlem  38498  heibor1  38502  infleinflem1  46126  limcrecl  46386  islpcn  46394  etransclem18  47007  etransclem46  47035  ioorrnopnlem  47059  sge0iunmptlemre  47170  itscnhlinecirc02p  49606