Theorem rpxr 13000

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℝ^*cxr 11212  ℝ⁺crp 12990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-un 3909  df-ss 3921  df-xr 11217  df-rp 12991

This theorem is referenced by:  xlemul1  13290  xlemul2  13291  xltmul1  13292  xltmul2  13293  modelico  13888  muladdmodid  13920  sgnrrp  15101  blcntrps  24452  blcntr  24453  blssexps  24466  blssex  24467  blin2  24469  neibl  24541  blnei  24542  metss  24548  metss2lem  24551  stdbdmet  24556  stdbdmopn  24558  metrest  24564  prdsxmslem2  24569  metcnp3  24580  metcnp  24581  metcnpi3  24586  txmetcnp  24587  metustid  24594  cfilucfil  24599  blval2  24602  elbl4  24603  metucn  24611  nmoix  24769  xrsmopn  24853  reperflem  24859  reconnlem2  24868  metdseq0  24895  cnllycmp  24998  lebnum  25006  xlebnum  25007  lebnumii  25008  nmhmcn  25162  lmmbr  25300  lmmbr2  25301  lmnn  25305  cfilfcls  25316  iscau2  25319  iscmet3lem2  25334  equivcfil  25341  flimcfil  25356  cmpcmet  25361  bcthlem5  25370  ellimc3  25921  pige3ALT  26562  efopnlem1  26698  efopnlem2  26699  efopn  26700  xrlimcnp  27010  efrlim  27011  lgamcvg2  27096  pntlemi  27645  pntlemp  27651  ubthlem1  31019  xdivpnfrp  33071  pnfinf  33324  signsply0  34809  cnllysconn  35559  poimirlem29  38112  heicant  38118  itg2gt0cn  38138  ftc1anc  38164  areacirclem1  38171  areacirc  38176  blssp  38219  sstotbnd2  38237  isbndx  38245  isbnd2  38246  isbnd3  38247  ssbnd  38251  prdstotbnd  38257  prdsbnd2  38258  cntotbnd  38259  ismtybndlem  38269  heibor1  38273  infleinflem1  45909  limcrecl  46169  islpcn  46177  etransclem18  46790  etransclem46  46818  ioorrnopnlem  46842  sge0iunmptlemre  46953  itscnhlinecirc02p  49371