MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfzelz Structured version   Unicode version

Theorem elfzelz 11439
Description: A member of a finite set of sequential integer is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
elfzelz  |-  ( K  e.  ( M ... N )  ->  K  e.  ZZ )

Proof of Theorem elfzelz
StepHypRef Expression
1 elfzuz 11435 . 2  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
2 eluzelz 10857 . 2  |-  ( K  e.  ( ZZ>= `  M
)  ->  K  e.  ZZ )
31, 2syl 16 1  |-  ( K  e.  ( M ... N )  ->  K  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   ` cfv 5406  (class class class)co 6080   ZZcz 10633   ZZ>=cuz 10848   ...cfz 11423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-cnex 9325  ax-resscn 9326
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-fv 5414  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-1st 6566  df-2nd 6567  df-neg 9585  df-z 10634  df-uz 10849  df-fz 11424
This theorem is referenced by:  elfz1eq  11448  fzsplit2  11460  fzdisj  11462  elfznn  11464  fznn0sub2  11474  fznatpl1  11494  fzrev2i  11504  fzrev3i  11506  fznuz  11525  fzrevral  11527  fzshftral  11530  fzosplit  11565  sermono  11821  seqf1olem1  11828  seqf1olem2  11829  bcval2  12064  bcval4  12066  bccmpl  12068  bcm1k  12074  bcp1nk  12076  bcval5  12077  bcpasc  12080  bccl2  12082  seqcoll  12199  seqcoll2  12200  swrdval2  12299  swrd0val  12300  addlenrevswrd  12313  swrd0fv  12318  ccatswrd  12333  swrdswrd  12337  swrdswrd0  12339  swrdccatin12lem2a  12359  swrdccatin12lem2b  12360  swrdccatin2  12361  swrdccatin12  12365  spllen  12379  splfv1  12380  cshwidxm  12427  cshwidxn  12428  lswcshw  12432  seqshft  12557  sumrblem  13171  summolem2a  13175  fsum0diaglem  13226  fsumrev  13228  fsumshft  13229  fsumshftm  13230  fsum0diag2  13232  binomlem  13274  binom11  13277  bcxmas  13280  arisum  13304  geo2sum  13315  mertenslem1  13326  fzm1ndvds  13567  hashdvds  13832  phiprmpw  13833  prmdiveq  13843  prmdivdiv  13844  modprminv  13852  modprminveq  13853  modprm0  13855  4sqlem11  13998  4sqlem12  13999  vdwapun  14017  cshwshashlem1  14104  cshwshashlem2  14105  dfod2  16044  efgredleme  16219  efgredlemc  16221  efgredlemb  16222  iscmet3  20645  mbfi1fseqlem4  21037  itgz  21099  itgcl  21102  ibl0  21105  iblss  21123  iblss2  21124  itgss  21130  itgeqa  21132  iblconst  21136  iblabsr  21148  iblmulc2  21149  itgsplit  21154  dvfsumlem3  21341  plyeq0lem  21562  aalioulem1  21682  cxpeq  22079  birthdaylem2  22230  wilthlem1  22290  wilthlem2  22291  wilthlem3  22292  ftalem5  22298  basellem3  22304  basellem4  22305  dvdsppwf1o  22410  dvdsflf1o  22411  musum  22415  ppiub  22427  chtublem  22434  mersenne  22450  bposlem1  22507  lgsval2lem  22529  lgsdilem2  22554  lgsqrlem2  22565  lgsqrlem4  22567  lgseisenlem1  22572  lgseisenlem2  22573  lgseisenlem3  22574  lgsquadlem1  22577  lgsquadlem2  22578  lgsquadlem3  22579  rpvmasumlem  22620  dchrisumlem1  22622  dchrisumlem2  22623  dchrmusum2  22627  dchrvmasumlem1  22628  dchrvmasum2lem  22629  dchrvmasum2if  22630  dchrvmasumlem3  22632  dchrvmasumiflem1  22634  dchrvmasumiflem2  22635  dchrisum0flblem1  22641  rpvmasum2  22645  dchrisum0lem1b  22648  dchrisum0lem1  22649  dchrisum0lem2a  22650  dchrisum0lem2  22651  dchrisum0lem3  22652  dchrmusumlem  22655  dchrvmasumlem  22656  logdivbnd  22689  pntpbnd1  22719  pntlemh  22732  pntlemj  22736  pntlemf  22738  ostth2lem2  22767  axlowdimlem13  23022  axlowdimlem14  23023  axlowdimlem16  23025  fargshiftfo  23346  fzsplit3  25900  bcm1n  25901  ballotlemfc0  26722  ballotlemfcc  26723  ballotlemodife  26727  ballotlemimin  26735  ballotlemsgt1  26740  ballotlemsel1i  26742  ballotlemsf1o  26743  ballotlemsi  26744  ballotlemsima  26745  ballotlemfg  26755  ballotlemfrc  26756  ballotlemfrceq  26758  ballotlemfrcn0  26759  ballotlemirc  26761  ballotlem1ri  26764  erdszelem8  26933  erdszelem9  26934  cvmliftlem7  27027  supfz  27232  inffz  27233  prodfn0  27255  prodrblem  27288  prodmolem2a  27293  fprodntriv  27301  fprodser  27308  fprod1p  27324  fprodshft  27333  fprodrev  27334  fallfacval3  27361  fallfacfwd  27385  0fallfac  27386  binomfallfaclem1  27388  binomfallfaclem2  27389  binomrisefac  27391  fallfacval4  27392  predfz  27510  bpolycl  28041  bpolysum  28042  bpolydiflem  28043  fsumkthpow  28045  bpoly4  28048  mblfinlem2  28270  iblmulc2nc  28298  fdc  28482  irrapxlem1  29005  irrapxlem2  29006  irrapxlem3  29007  pellexlem5  29016  acongrep  29165  fzmaxdif  29166  acongeq  29168  jm2.22  29186  jm2.23  29187  jm2.26lem3  29192  jm2.26  29193  jm2.27dlem2  29201  fmul01lt1lem1  29607  fmul01lt1lem2  29608  stoweidlem3  29641  stoweidlem11  29649  stoweidlem20  29658  stoweidlem26  29664  stoweidlem34  29672  stoweidlem59  29697  stirlinglem10  29721  2elfz2melfz  30045  elfzelfzlble  30052  clwwnisshclwwn  30316  erclwwlksym0  30321  erclwwlktr0  30322  erclwwlkeqlen  30325  difelfznle  30331  cshwlemma1  30332  eleclclwwlknlem2  30334  erclwwlkneqlen  30341  clwlkfclwwlk  30360
  Copyright terms: Public domain W3C validator