Theorem rpxr 12915

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝ^*cxr 11165  ℝ⁺crp 12905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-un 3906  df-ss 3918  df-xr 11170  df-rp 12906

This theorem is referenced by:  xlemul1  13205  xlemul2  13206  xltmul1  13207  xltmul2  13208  modelico  13801  muladdmodid  13833  sgnrrp  15014  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  25214  lmmbr2  25215  lmnn  25219  cfilfcls  25230  iscau2  25233  iscmet3lem2  25248  equivcfil  25255  flimcfil  25270  cmpcmet  25275  bcthlem5  25284  ellimc3  25836  pige3ALT  26485  efopnlem1  26621  efopnlem2  26622  efopn  26623  xrlimcnp  26934  efrlim  26935  efrlimOLD  26936  lgamcvg2  27021  pntlemi  27571  pntlemp  27577  ubthlem1  30945  xdivpnfrp  33014  pnfinf  33265  signsply0  34708  cnllysconn  35439  poimirlem29  37846  heicant  37852  itg2gt0cn  37872  ftc1anc  37898  areacirclem1  37905  areacirc  37910  blssp  37953  sstotbnd2  37971  isbndx  37979  isbnd2  37980  isbnd3  37981  ssbnd  37985  prdstotbnd  37991  prdsbnd2  37992  cntotbnd  37993  ismtybndlem  38003  heibor1  38007  infleinflem1  45610  limcrecl  45871  islpcn  45879  etransclem18  46492  etransclem46  46520  ioorrnopnlem  46544  sge0iunmptlemre  46655  itscnhlinecirc02p  49027