Theorem rpxr 12399

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝ^*cxr 10674  ℝ⁺crp 12390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-xr 10679  df-rp 12391

This theorem is referenced by:  xlemul1  12684  xlemul2  12685  xltmul1  12686  xltmul2  12687  modelico  13250  muladdmodid  13280  sgnrrp  14450  blcntrps  23022  blcntr  23023  blssexps  23036  blssex  23037  blin2  23039  neibl  23111  blnei  23112  metss  23118  metss2lem  23121  stdbdmet  23126  stdbdmopn  23128  metrest  23134  prdsxmslem2  23139  metcnp3  23150  metcnp  23151  metcnpi3  23156  txmetcnp  23157  metustid  23164  cfilucfil  23169  blval2  23172  elbl4  23173  metucn  23181  nmoix  23338  xrsmopn  23420  reperflem  23426  reconnlem2  23435  metdseq0  23462  cnllycmp  23560  lebnum  23568  xlebnum  23569  lebnumii  23570  nmhmcn  23724  lmmbr  23861  lmmbr2  23862  lmnn  23866  cfilfcls  23877  iscau2  23880  iscmet3lem2  23895  equivcfil  23902  flimcfil  23917  cmpcmet  23922  bcthlem5  23931  ellimc3  24477  pige3ALT  25105  efopnlem1  25239  efopnlem2  25240  efopn  25241  xrlimcnp  25546  efrlim  25547  lgamcvg2  25632  pntlemi  26180  pntlemp  26186  ubthlem1  28647  xdivpnfrp  30609  pnfinf  30812  signsply0  31821  cnllysconn  32492  poimirlem29  34936  heicant  34942  itg2gt0cn  34962  ftc1anc  34990  areacirclem1  34997  areacirc  35002  blssp  35046  sstotbnd2  35067  isbndx  35075  isbnd2  35076  isbnd3  35077  ssbnd  35081  prdstotbnd  35087  prdsbnd2  35088  cntotbnd  35089  ismtybndlem  35099  heibor1  35103  infleinflem1  41658  limcrecl  41930  islpcn  41940  etransclem18  42557  etransclem46  42585  ioorrnopnlem  42609  sge0iunmptlemre  42717  itscnhlinecirc02p  44792