Theorem rpxr 13023

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝ^*cxr 11273  ℝ⁺crp 13013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-un 3936  df-ss 3948  df-xr 11278  df-rp 13014

This theorem is referenced by:  xlemul1  13311  xlemul2  13312  xltmul1  13313  xltmul2  13314  modelico  13903  muladdmodid  13933  sgnrrp  15115  blcntrps  24356  blcntr  24357  blssexps  24370  blssex  24371  blin2  24373  neibl  24445  blnei  24446  metss  24452  metss2lem  24455  stdbdmet  24460  stdbdmopn  24462  metrest  24468  prdsxmslem2  24473  metcnp3  24484  metcnp  24485  metcnpi3  24490  txmetcnp  24491  metustid  24498  cfilucfil  24503  blval2  24506  elbl4  24507  metucn  24515  nmoix  24673  xrsmopn  24757  reperflem  24763  reconnlem2  24772  metdseq0  24799  cnllycmp  24911  lebnum  24919  xlebnum  24920  lebnumii  24921  nmhmcn  25076  lmmbr  25215  lmmbr2  25216  lmnn  25220  cfilfcls  25231  iscau2  25234  iscmet3lem2  25249  equivcfil  25256  flimcfil  25271  cmpcmet  25276  bcthlem5  25285  ellimc3  25837  pige3ALT  26486  efopnlem1  26622  efopnlem2  26623  efopn  26624  xrlimcnp  26935  efrlim  26936  efrlimOLD  26937  lgamcvg2  27022  pntlemi  27572  pntlemp  27578  ubthlem1  30856  xdivpnfrp  32912  pnfinf  33186  signsply0  34588  cnllysconn  35272  poimirlem29  37678  heicant  37684  itg2gt0cn  37704  ftc1anc  37730  areacirclem1  37737  areacirc  37742  blssp  37785  sstotbnd2  37803  isbndx  37811  isbnd2  37812  isbnd3  37813  ssbnd  37817  prdstotbnd  37823  prdsbnd2  37824  cntotbnd  37825  ismtybndlem  37835  heibor1  37839  infleinflem1  45377  limcrecl  45638  islpcn  45648  etransclem18  46261  etransclem46  46289  ioorrnopnlem  46313  sge0iunmptlemre  46424  itscnhlinecirc02p  48745