Theorem rpxr 11840

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

Syntax hints:   → wi 4   ∈ wcel 1990  ℝ^*cxr 10073  ℝ⁺crp 11832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-xr 10078  df-rp 11833

This theorem is referenced by:  xlemul1  12120  xlemul2  12121  xltmul1  12122  xltmul2  12123  modelico  12680  muladdmodid  12710  sgnrrp  13831  blcntrps  22217  blcntr  22218  unirnblps  22224  unirnbl  22225  blssexps  22231  blssex  22232  blin2  22234  neibl  22306  blnei  22307  metss  22313  metss2lem  22316  stdbdmet  22321  stdbdmopn  22323  mopnex  22324  metrest  22329  prdsxmslem2  22334  metcnp3  22345  metcnp  22346  metcnpi3  22351  txmetcnp  22352  metustid  22359  cfilucfil  22364  blval2  22367  elbl4  22368  metucn  22376  dscopn  22378  nmoix  22533  xrsmopn  22615  zdis  22619  reperflem  22621  reconnlem2  22630  metdseq0  22657  cnllycmp  22755  lebnum  22763  xlebnum  22764  lebnumii  22765  nmhmcn  22920  lmmbr  23056  lmmbr2  23057  lmnn  23061  cfilfcls  23072  iscau2  23075  iscmet3lem2  23090  equivcfil  23097  flimcfil  23112  cmpcmet  23116  cncmet  23119  bcthlem5  23125  ellimc3  23643  abelthlem2  24186  abelthlem5  24189  abelthlem7  24192  pige3  24269  dvlog2  24399  efopnlem1  24402  efopnlem2  24403  efopn  24404  logtayl  24406  logtayl2  24408  xrlimcnp  24695  efrlim  24696  lgamcvg2  24781  pntlemi  25293  pntlemp  25299  ubthlem1  27726  xdivpnfrp  29641  pnfinf  29737  signsply0  30628  cnllysconn  31227  poimirlem29  33438  heicant  33444  itg2gt0cn  33465  ftc1anc  33493  areacirclem1  33500  areacirc  33505  blssp  33552  sstotbnd2  33573  isbndx  33581  isbnd2  33582  isbnd3  33583  ssbnd  33587  prdstotbnd  33593  prdsbnd2  33594  cntotbnd  33595  ismtybndlem  33605  heibor1  33609  infleinflem1  39586  limcrecl  39861  islpcn  39871  etransclem18  40469  etransclem46  40497  ioorrnopnlem  40524  sge0iunmptlemre  40632