Theorem rpxr 12039

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

Syntax hints:   → wi 4   ∈ wcel 2155  ℝ^*cxr 10327  ℝ⁺crp 12028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rab 3064  df-v 3352  df-un 3737  df-in 3739  df-ss 3746  df-xr 10332  df-rp 12029

This theorem is referenced by:  xlemul1  12322  xlemul2  12323  xltmul1  12324  xltmul2  12325  modelico  12888  muladdmodid  12918  sgnrrp  14118  blcntrps  22496  blcntr  22497  unirnblps  22503  unirnbl  22504  blssexps  22510  blssex  22511  blin2  22513  neibl  22585  blnei  22586  metss  22592  metss2lem  22595  stdbdmet  22600  stdbdmopn  22602  mopnex  22603  metrest  22608  prdsxmslem2  22613  metcnp3  22624  metcnp  22625  metcnpi3  22630  txmetcnp  22631  metustid  22638  cfilucfil  22643  blval2  22646  elbl4  22647  metucn  22655  dscopn  22657  nmoix  22812  xrsmopn  22894  zdis  22898  reperflem  22900  reconnlem2  22909  metdseq0  22936  cnllycmp  23034  lebnum  23042  xlebnum  23043  lebnumii  23044  nmhmcn  23198  lmmbr  23335  lmmbr2  23336  lmnn  23340  cfilfcls  23351  iscau2  23354  iscmet3lem2  23369  equivcfil  23376  flimcfil  23391  cmpcmet  23396  cncmet  23399  bcthlem5  23405  ellimc3  23934  abelthlem2  24477  abelthlem5  24480  abelthlem7  24483  pige3  24561  dvlog2  24690  efopnlem1  24693  efopnlem2  24694  efopn  24695  logtayl  24697  logtayl2  24699  xrlimcnp  24986  efrlim  24987  lgamcvg2  25072  pntlemi  25584  pntlemp  25590  ubthlem1  28117  xdivpnfrp  30023  pnfinf  30119  signsply0  31011  cnllysconn  31607  poimirlem29  33794  heicant  33800  itg2gt0cn  33820  ftc1anc  33848  areacirclem1  33855  areacirc  33860  blssp  33906  sstotbnd2  33927  isbndx  33935  isbnd2  33936  isbnd3  33937  ssbnd  33941  prdstotbnd  33947  prdsbnd2  33948  cntotbnd  33949  ismtybndlem  33959  heibor1  33963  infleinflem1  40156  limcrecl  40431  islpcn  40441  etransclem18  41038  etransclem46  41066  ioorrnopnlem  41093  sge0iunmptlemre  41201