Theorem rpxr 12044

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℝ^*cxr 10276  ℝ⁺crp 12036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-un 3729  df-in 3731  df-ss 3738  df-xr 10281  df-rp 12037

This theorem is referenced by:  xlemul1  12326  xlemul2  12327  xltmul1  12328  xltmul2  12329  modelico  12889  muladdmodid  12919  sgnrrp  14040  blcntrps  22438  blcntr  22439  unirnblps  22445  unirnbl  22446  blssexps  22452  blssex  22453  blin2  22455  neibl  22527  blnei  22528  metss  22534  metss2lem  22537  stdbdmet  22542  stdbdmopn  22544  mopnex  22545  metrest  22550  prdsxmslem2  22555  metcnp3  22566  metcnp  22567  metcnpi3  22572  txmetcnp  22573  metustid  22580  cfilucfil  22585  blval2  22588  elbl4  22589  metucn  22597  dscopn  22599  nmoix  22754  xrsmopn  22836  zdis  22840  reperflem  22842  reconnlem2  22851  metdseq0  22878  cnllycmp  22976  lebnum  22984  xlebnum  22985  lebnumii  22986  nmhmcn  23140  lmmbr  23276  lmmbr2  23277  lmnn  23281  cfilfcls  23292  iscau2  23295  iscmet3lem2  23310  equivcfil  23317  flimcfil  23332  cmpcmet  23336  cncmet  23339  bcthlem5  23345  ellimc3  23864  abelthlem2  24407  abelthlem5  24410  abelthlem7  24413  pige3  24491  dvlog2  24621  efopnlem1  24624  efopnlem2  24625  efopn  24626  logtayl  24628  logtayl2  24630  xrlimcnp  24917  efrlim  24918  lgamcvg2  25003  pntlemi  25515  pntlemp  25521  ubthlem1  28067  xdivpnfrp  29982  pnfinf  30078  signsply0  30969  cnllysconn  31566  poimirlem29  33772  heicant  33778  itg2gt0cn  33798  ftc1anc  33826  areacirclem1  33833  areacirc  33838  blssp  33885  sstotbnd2  33906  isbndx  33914  isbnd2  33915  isbnd3  33916  ssbnd  33920  prdstotbnd  33926  prdsbnd2  33927  cntotbnd  33928  ismtybndlem  33938  heibor1  33942  infleinflem1  40103  limcrecl  40380  islpcn  40390  etransclem18  40987  etransclem46  41015  ioorrnopnlem  41042  sge0iunmptlemre  41150