Theorem rpxr 11716

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℝ^*cxr 9952  ℝ⁺crp 11708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-xr 9957  df-rp 11709

This theorem is referenced by:  xlemul1  11992  xlemul2  11993  xltmul1  11994  xltmul2  11995  modelico  12542  muladdmodid  12572  sgnrrp  13679  blcntrps  22027  blcntr  22028  unirnblps  22034  unirnbl  22035  blssexps  22041  blssex  22042  blin2  22044  neibl  22116  blnei  22117  metss  22123  metss2lem  22126  stdbdmet  22131  stdbdmopn  22133  mopnex  22134  metrest  22139  prdsxmslem2  22144  metcnp3  22155  metcnp  22156  metcnpi3  22161  txmetcnp  22162  metustid  22169  cfilucfil  22174  blval2  22177  elbl4  22178  metucn  22186  dscopn  22188  nmoix  22343  xrsmopn  22423  zdis  22427  reperflem  22429  reconnlem2  22438  metdseq0  22465  cnllycmp  22563  lebnum  22571  xlebnum  22572  lebnumii  22573  nmhmcn  22728  lmmbr  22864  lmmbr2  22865  lmnn  22869  cfilfcls  22880  iscau2  22883  iscmet3lem2  22898  equivcfil  22905  flimcfil  22920  cmpcmet  22924  cncmet  22927  bcthlem5  22933  ellimc3  23449  abelthlem2  23990  abelthlem5  23993  abelthlem7  23996  pige3  24073  dvlog2  24199  efopnlem1  24202  efopnlem2  24203  efopn  24204  logtayl  24206  logtayl2  24208  xrlimcnp  24495  efrlim  24496  lgamcvg2  24581  pntlemi  25093  pntlemp  25099  ubthlem1  27110  xdivpnfrp  28972  pnfinf  29068  signsply0  29954  cnllyscon  30481  poimirlem29  32608  heicant  32614  itg2gt0cn  32635  ftc1anc  32663  areacirclem1  32670  areacirc  32675  blssp  32722  sstotbnd2  32743  isbndx  32751  isbnd2  32752  isbnd3  32753  ssbnd  32757  prdstotbnd  32763  prdsbnd2  32764  cntotbnd  32765  ismtybndlem  32775  heibor1  32779  infleinflem1  38527  limcrecl  38696  islpcn  38706  etransclem18  39145  etransclem46  39173  ioorrnopnlem  39200  sge0iunmptlemre  39308