Theorem rpxr 12902

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝ^*cxr 11152  ℝ⁺crp 12892

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-un 3903  df-ss 3915  df-xr 11157  df-rp 12893

This theorem is referenced by:  xlemul1  13191  xlemul2  13192  xltmul1  13193  xltmul2  13194  modelico  13787  muladdmodid  13819  sgnrrp  15000  blcntrps  24328  blcntr  24329  blssexps  24342  blssex  24343  blin2  24345  neibl  24417  blnei  24418  metss  24424  metss2lem  24427  stdbdmet  24432  stdbdmopn  24434  metrest  24440  prdsxmslem2  24445  metcnp3  24456  metcnp  24457  metcnpi3  24462  txmetcnp  24463  metustid  24470  cfilucfil  24475  blval2  24478  elbl4  24479  metucn  24487  nmoix  24645  xrsmopn  24729  reperflem  24735  reconnlem2  24744  metdseq0  24771  cnllycmp  24883  lebnum  24891  xlebnum  24892  lebnumii  24893  nmhmcn  25048  lmmbr  25186  lmmbr2  25187  lmnn  25191  cfilfcls  25202  iscau2  25205  iscmet3lem2  25220  equivcfil  25227  flimcfil  25242  cmpcmet  25247  bcthlem5  25256  ellimc3  25808  pige3ALT  26457  efopnlem1  26593  efopnlem2  26594  efopn  26595  xrlimcnp  26906  efrlim  26907  efrlimOLD  26908  lgamcvg2  26993  pntlemi  27543  pntlemp  27549  ubthlem1  30852  xdivpnfrp  32920  pnfinf  33159  signsply0  34585  cnllysconn  35310  poimirlem29  37709  heicant  37715  itg2gt0cn  37735  ftc1anc  37761  areacirclem1  37768  areacirc  37773  blssp  37816  sstotbnd2  37834  isbndx  37842  isbnd2  37843  isbnd3  37844  ssbnd  37848  prdstotbnd  37854  prdsbnd2  37855  cntotbnd  37856  ismtybndlem  37866  heibor1  37870  infleinflem1  45492  limcrecl  45753  islpcn  45761  etransclem18  46374  etransclem46  46402  ioorrnopnlem  46426  sge0iunmptlemre  46537  itscnhlinecirc02p  48910