Theorem rpxr 13045

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝ^*cxr 11295  ℝ⁺crp 13035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-un 3955  df-ss 3967  df-xr 11300  df-rp 13036

This theorem is referenced by:  xlemul1  13333  xlemul2  13334  xltmul1  13335  xltmul2  13336  modelico  13922  muladdmodid  13952  sgnrrp  15131  blcntrps  24423  blcntr  24424  blssexps  24437  blssex  24438  blin2  24440  neibl  24515  blnei  24516  metss  24522  metss2lem  24525  stdbdmet  24530  stdbdmopn  24532  metrest  24538  prdsxmslem2  24543  metcnp3  24554  metcnp  24555  metcnpi3  24560  txmetcnp  24561  metustid  24568  cfilucfil  24573  blval2  24576  elbl4  24577  metucn  24585  nmoix  24751  xrsmopn  24835  reperflem  24841  reconnlem2  24850  metdseq0  24877  cnllycmp  24989  lebnum  24997  xlebnum  24998  lebnumii  24999  nmhmcn  25154  lmmbr  25293  lmmbr2  25294  lmnn  25298  cfilfcls  25309  iscau2  25312  iscmet3lem2  25327  equivcfil  25334  flimcfil  25349  cmpcmet  25354  bcthlem5  25363  ellimc3  25915  pige3ALT  26563  efopnlem1  26699  efopnlem2  26700  efopn  26701  xrlimcnp  27012  efrlim  27013  efrlimOLD  27014  lgamcvg2  27099  pntlemi  27649  pntlemp  27655  ubthlem1  30890  xdivpnfrp  32916  pnfinf  33191  signsply0  34567  cnllysconn  35251  poimirlem29  37657  heicant  37663  itg2gt0cn  37683  ftc1anc  37709  areacirclem1  37716  areacirc  37721  blssp  37764  sstotbnd2  37782  isbndx  37790  isbnd2  37791  isbnd3  37792  ssbnd  37796  prdstotbnd  37802  prdsbnd2  37803  cntotbnd  37804  ismtybndlem  37814  heibor1  37818  infleinflem1  45386  limcrecl  45649  islpcn  45659  etransclem18  46272  etransclem46  46300  ioorrnopnlem  46324  sge0iunmptlemre  46435  itscnhlinecirc02p  48711