Theorem rpxr 13027

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℝ^*cxr 11243  ℝ⁺crp 13017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-un 3911  df-ss 3923  df-xr 11248  df-rp 13018

This theorem is referenced by:  xlemul1  13317  xlemul2  13318  xltmul1  13319  xltmul2  13320  modelico  13916  muladdmodid  13948  sgnrrp  15130  blcntrps  24550  blcntr  24551  blssexps  24564  blssex  24565  blin2  24567  neibl  24639  blnei  24640  metss  24646  metss2lem  24649  stdbdmet  24654  stdbdmopn  24656  metrest  24662  prdsxmslem2  24667  metcnp3  24678  metcnp  24679  metcnpi3  24684  txmetcnp  24685  metustid  24692  cfilucfil  24697  blval2  24700  elbl4  24701  metucn  24709  nmoix  24867  xrsmopn  24951  reperflem  24957  reconnlem2  24966  metdseq0  24993  cnllycmp  25096  lebnum  25104  xlebnum  25105  lebnumii  25106  nmhmcn  25260  lmmbr  25398  lmmbr2  25399  lmnn  25403  cfilfcls  25414  iscau2  25417  iscmet3lem2  25432  equivcfil  25439  flimcfil  25454  cmpcmet  25459  bcthlem5  25468  ellimc3  26019  pige3ALT  26663  efopnlem1  26799  efopnlem2  26800  efopn  26801  xrlimcnp  27111  efrlim  27112  lgamcvg2  27197  pntlemi  27746  pntlemp  27752  ubthlem1  31200  xdivpnfrp  33230  pnfinf  33481  signsply0  34916  cnllysconn  35715  poimirlem29  38278  heicant  38284  itg2gt0cn  38304  ftc1anc  38330  areacirclem1  38337  areacirc  38342  blssp  38385  sstotbnd2  38403  isbndx  38411  isbnd2  38412  isbnd3  38413  ssbnd  38417  prdstotbnd  38423  prdsbnd2  38424  cntotbnd  38425  ismtybndlem  38435  heibor1  38439  infleinflem1  46065  limcrecl  46325  islpcn  46333  etransclem18  46946  etransclem46  46974  ioorrnopnlem  46998  sge0iunmptlemre  47109  itscnhlinecirc02p  49542