Theorem rpxr 12392

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

Syntax hints:   → wi 4   ∈ wcel 2110  ℝ^*cxr 10668  ℝ⁺crp 12383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-un 3941  df-in 3943  df-ss 3952  df-xr 10673  df-rp 12384

This theorem is referenced by:  xlemul1  12677  xlemul2  12678  xltmul1  12679  xltmul2  12680  modelico  13243  muladdmodid  13273  sgnrrp  14444  blcntrps  23016  blcntr  23017  blssexps  23030  blssex  23031  blin2  23033  neibl  23105  blnei  23106  metss  23112  metss2lem  23115  stdbdmet  23120  stdbdmopn  23122  metrest  23128  prdsxmslem2  23133  metcnp3  23144  metcnp  23145  metcnpi3  23150  txmetcnp  23151  metustid  23158  cfilucfil  23163  blval2  23166  elbl4  23167  metucn  23175  nmoix  23332  xrsmopn  23414  reperflem  23420  reconnlem2  23429  metdseq0  23456  cnllycmp  23554  lebnum  23562  xlebnum  23563  lebnumii  23564  nmhmcn  23718  lmmbr  23855  lmmbr2  23856  lmnn  23860  cfilfcls  23871  iscau2  23874  iscmet3lem2  23889  equivcfil  23896  flimcfil  23911  cmpcmet  23916  bcthlem5  23925  ellimc3  24471  pige3ALT  25099  efopnlem1  25233  efopnlem2  25234  efopn  25235  xrlimcnp  25540  efrlim  25541  lgamcvg2  25626  pntlemi  26174  pntlemp  26180  ubthlem1  28641  xdivpnfrp  30604  pnfinf  30807  signsply0  31816  cnllysconn  32487  poimirlem29  34915  heicant  34921  itg2gt0cn  34941  ftc1anc  34969  areacirclem1  34976  areacirc  34981  blssp  35025  sstotbnd2  35046  isbndx  35054  isbnd2  35055  isbnd3  35056  ssbnd  35060  prdstotbnd  35066  prdsbnd2  35067  cntotbnd  35068  ismtybndlem  35078  heibor1  35082  infleinflem1  41630  limcrecl  41902  islpcn  41912  etransclem18  42530  etransclem46  42558  ioorrnopnlem  42582  sge0iunmptlemre  42690  itscnhlinecirc02p  44765