Theorem rpxr 12248

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

Syntax hints:   → wi 4   ∈ wcel 2081  ℝ^*cxr 10520  ℝ⁺crp 12239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rab 3114  df-v 3439  df-un 3864  df-in 3866  df-ss 3874  df-xr 10525  df-rp 12240

This theorem is referenced by:  xlemul1  12533  xlemul2  12534  xltmul1  12535  xltmul2  12536  modelico  13099  muladdmodid  13129  sgnrrp  14284  blcntrps  22705  blcntr  22706  blssexps  22719  blssex  22720  blin2  22722  neibl  22794  blnei  22795  metss  22801  metss2lem  22804  stdbdmet  22809  stdbdmopn  22811  metrest  22817  prdsxmslem2  22822  metcnp3  22833  metcnp  22834  metcnpi3  22839  txmetcnp  22840  metustid  22847  cfilucfil  22852  blval2  22855  elbl4  22856  metucn  22864  nmoix  23021  xrsmopn  23103  reperflem  23109  reconnlem2  23118  metdseq0  23145  cnllycmp  23243  lebnum  23251  xlebnum  23252  lebnumii  23253  nmhmcn  23407  lmmbr  23544  lmmbr2  23545  lmnn  23549  cfilfcls  23560  iscau2  23563  iscmet3lem2  23578  equivcfil  23585  flimcfil  23600  cmpcmet  23605  bcthlem5  23614  ellimc3  24160  pige3ALT  24788  efopnlem1  24920  efopnlem2  24921  efopn  24922  xrlimcnp  25228  efrlim  25229  lgamcvg2  25314  pntlemi  25862  pntlemp  25868  ubthlem1  28338  xdivpnfrp  30293  pnfinf  30450  signsply0  31438  cnllysconn  32100  poimirlem29  34452  heicant  34458  itg2gt0cn  34478  ftc1anc  34506  areacirclem1  34513  areacirc  34518  blssp  34563  sstotbnd2  34584  isbndx  34592  isbnd2  34593  isbnd3  34594  ssbnd  34598  prdstotbnd  34604  prdsbnd2  34605  cntotbnd  34606  ismtybndlem  34616  heibor1  34620  infleinflem1  41179  limcrecl  41452  islpcn  41462  etransclem18  42079  etransclem46  42107  ioorrnopnlem  42131  sge0iunmptlemre  42239  itscnhlinecirc02p  44253