MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexr Structured version   Visualization version   GIF version

Theorem rexr 10676
Description: A standard real is an extended real. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
rexr (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)

Proof of Theorem rexr
StepHypRef Expression
1 ressxr 10674 . 2 ℝ ⊆ ℝ*
21sseli 3911 1 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  cr 10525  *cxr 10663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-xr 10668
This theorem is referenced by:  rexri  10688  lenlt  10708  ltpnf  12503  mnflt  12506  xrltnsym  12518  xrlttr  12521  xrre  12550  xrre3  12552  max1  12566  max2  12568  min1  12570  min2  12571  maxle  12572  lemin  12573  maxlt  12574  ltmin  12575  max0sub  12577  qbtwnxr  12581  xralrple  12586  alrple  12587  xltnegi  12597  rexadd  12613  xaddnemnf  12617  xaddnepnf  12618  xaddcom  12621  xnegdi  12629  xpncan  12632  xnpcan  12633  xleadd1a  12634  xleadd1  12636  xltadd1  12637  xltadd2  12638  xsubge0  12642  rexmul  12652  xadddilem  12675  xadddir  12677  xrsupsslem  12688  xrinfmsslem  12689  xrub  12693  supxrun  12697  supxrunb1  12700  supxrunb2  12701  supxrbnd1  12702  supxrbnd2  12703  xrsup0  12704  supxrbnd  12709  infmremnf  12724  elioo4g  12785  elioc2  12788  elico2  12789  elicc2  12790  iccss  12793  iooshf  12804  iooneg  12849  icoshft  12851  difreicc  12862  hashbnd  13692  elicc4abs  14671  icodiamlt  14787  limsupgord  14821  pcadd  16215  ramubcl  16344  lt6abl  19008  xrsmcmn  20114  xrs1mnd  20129  xrs10  20130  xrsdsreval  20136  psmetge0  22919  xmetge0  22951  imasdsf1olem  22980  bl2in  23007  blssps  23031  blss  23032  blcld  23112  icopnfcld  23373  iocmnfcld  23374  bl2ioo  23397  blssioo  23400  xrtgioo  23411  xrsblre  23416  iccntr  23426  icccmplem2  23428  icccmp  23430  reconnlem2  23432  xrge0tsms  23439  icoopnst  23544  iocopnst  23545  ovolfioo  24071  ovolicc2lem1  24121  ovolicc2lem5  24125  voliunlem3  24156  icombl1  24167  icombl  24168  iccvolcl  24171  ovolioo  24172  ioovolcl  24174  uniiccdif  24182  volsup2  24209  mbfimasn  24236  ismbf3d  24258  mbfsup  24268  itg2seq  24346  bddiblnc  24445  dvlip2  24598  ply1remlem  24763  abelthlem3  25028  abelth  25036  sincosq2sgn  25092  sincosq3sgn  25093  sinq12ge0  25101  sincos6thpi  25108  sineq0  25116  efif1olem1  25134  efif1olem2  25135  efif1o  25138  eff1o  25141  loglesqrt  25347  basellem1  25666  pntlemo  26191  nmobndi  28558  nmopub2tALT  29692  nmfnleub2  29709  nmopcoadji  29884  rexdiv  30628  xrge0tsmsd  30742  pnfneige0  31304  lmxrge0  31305  hashf2  31453  sxbrsigalem0  31639  orvcgteel  31835  orvclteel  31840  sgnclre  31907  sgnneg  31908  signstfvn  31949  signstfvneq0  31952  signsvfn  31962  ivthALT  33796  icorempo  34768  icoreunrn  34776  iooelexlt  34779  relowlssretop  34780  relowlpssretop  34781  poimir  35090  mblfinlem2  35095  iblabsnclem  35120  ftc1anclem1  35130  ftc1anclem6  35135  areacirclem5  35149  areacirc  35150  blbnd  35225  iocmbl  40161  reabssgn  40334  supxrre3  41955  supxrgere  41963  infrpge  41981  infxrunb2  41998  infxrbnd2  41999  infleinflem2  42001  xrralrecnnle  42015  supxrunb3  42034  supminfxr2  42106  xrpnf  42123  ioomidp  42149  limsupre  42281  limsupub  42344  limsuppnflem  42350  limsupre3lem  42372  liminfgord  42394  liminflelimsuplem  42415  limsupgtlem  42417  limsupub2  42452  xlimpnfxnegmnf  42454  xlimmnfvlem2  42473  xlimmnfv  42474  xlimpnfvlem2  42477  xlimpnfv  42478  icccncfext  42527  volioc  42612  volico  42623  fourierdlem113  42859  meaiuninclem  43117  meaiuninc3v  43121  icoresmbl  43180  ovolval5lem1  43289  mbfresmf  43371  cnfsmf  43372  incsmf  43374  smfconst  43381  decsmf  43398  smfres  43420  smfco  43432  issmfle2d  43438  bgoldbtbndlem3  44323  rrxsphere  45160
  Copyright terms: Public domain W3C validator