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

Theorem elfzelz 11677
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 11673 . 2  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
2 eluzelz 11080 . 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 1762   ` cfv 5579  (class class class)co 6275   ZZcz 10853   ZZ>=cuz 11071   ...cfz 11661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-cnex 9537  ax-resscn 9538
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-fv 5587  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-1st 6774  df-2nd 6775  df-neg 9797  df-z 10854  df-uz 11072  df-fz 11662
This theorem is referenced by:  elfz1eq  11686  fzsplit2  11699  fzdisj  11701  elfznn  11703  fznatpl1  11723  fzrev2i  11733  fzrev3i  11735  fznuz  11749  fzrevral  11751  fzshftral  11754  fznn0sub2  11768  difelfznle  11775  fzosplit  11815  sermono  12095  seqf1olem1  12102  seqf1olem2  12103  bcval2  12338  bcval4  12340  bccmpl  12342  bcm1k  12348  bcp1nk  12350  bcval5  12351  bcpasc  12354  bccl2  12356  seqcoll  12465  seqcoll2  12466  swrdval2  12597  swrd0val  12598  addlenrevswrd  12611  swrd0fv  12616  ccatswrd  12631  swrdswrd  12635  swrdswrd0  12637  swrdccatin12lem2a  12660  swrdccatin12lem2b  12661  swrdccatin2  12662  swrdccatin12  12666  spllen  12680  splfv1  12681  cshwidxm  12728  cshwidxn  12729  lswcshw  12733  2cshwcshw  12743  cshwcshid  12745  cshwcsh2id  12746  seqshft  12868  sumrblem  13482  summolem2a  13486  fsum0diaglem  13540  mptfzshft  13542  fsumrev  13543  fsumshftm  13545  fsum0diag2  13547  binomlem  13593  binom11  13596  bcxmas  13599  arisum  13623  geo2sum  13634  mertenslem1  13645  fzm1ndvds  13886  hashdvds  14153  phiprmpw  14154  prmdiveq  14164  prmdivdiv  14165  modprminv  14174  modprminveq  14175  modprm0  14178  4sqlem11  14321  4sqlem12  14322  vdwapun  14340  cshwshashlem1  14427  cshwshashlem2  14428  dfod2  16375  efgredleme  16550  efgredlemc  16552  efgredlemb  16553  gsummptshft  16740  srgbinomlem3  16974  srgbinomlem4  16975  srgbinomlem  16976  chpscmatgsummon  19106  cayhamlem1  19127  iscmet3  21460  mbfi1fseqlem4  21853  itgz  21915  itgcl  21918  ibl0  21921  iblss  21939  iblss2  21940  itgss  21946  itgeqa  21948  iblconst  21952  iblabsr  21964  iblmulc2  21965  itgsplit  21970  dvfsumlem3  22157  plyeq0lem  22335  aalioulem1  22455  cxpeq  22852  birthdaylem2  23003  wilthlem1  23063  wilthlem2  23064  wilthlem3  23065  ftalem5  23071  basellem3  23077  basellem4  23078  dvdsppwf1o  23183  dvdsflf1o  23184  musum  23188  ppiub  23200  chtublem  23207  mersenne  23223  bposlem1  23280  lgsval2lem  23302  lgsdilem2  23327  lgsqrlem2  23338  lgsqrlem4  23340  lgseisenlem1  23345  lgseisenlem2  23346  lgseisenlem3  23347  lgsquadlem1  23350  lgsquadlem2  23351  lgsquadlem3  23352  rpvmasumlem  23393  dchrisumlem1  23395  dchrisumlem2  23396  dchrmusum2  23400  dchrvmasumlem1  23401  dchrvmasum2lem  23402  dchrvmasum2if  23403  dchrvmasumlem3  23405  dchrvmasumiflem1  23407  dchrvmasumiflem2  23408  dchrisum0flblem1  23414  rpvmasum2  23418  dchrisum0lem1b  23421  dchrisum0lem1  23422  dchrisum0lem2a  23423  dchrisum0lem2  23424  dchrisum0lem3  23425  dchrmusumlem  23428  dchrvmasumlem  23429  logdivbnd  23462  pntpbnd1  23492  pntlemh  23505  pntlemj  23509  pntlemf  23511  ostth2lem2  23540  axlowdimlem13  23926  axlowdimlem14  23927  axlowdimlem16  23929  fargshiftfo  24300  clwwnisshclwwn  24471  erclwwlkeqlen  24474  eleclclwwlknlem2  24480  erclwwlkneqlen  24486  clwlkfclwwlk  24506  fzsplit3  27117  bcm1n  27118  ballotlemfc0  27921  ballotlemfcc  27922  ballotlemodife  27926  ballotlemimin  27934  ballotlemsgt1  27939  ballotlemsel1i  27941  ballotlemsf1o  27942  ballotlemsi  27943  ballotlemsima  27944  ballotlemfg  27954  ballotlemfrc  27955  ballotlemfrceq  27957  ballotlemfrcn0  27958  ballotlemirc  27960  ballotlem1ri  27963  erdszelem8  28132  erdszelem9  28133  cvmliftlem7  28226  supfz  28432  inffz  28433  prodfn0  28455  prodrblem  28488  prodmolem2a  28493  fprodntriv  28501  fprodser  28508  fprod1p  28524  fprodshft  28533  fprodrev  28534  fallfacval3  28561  fallfacfwd  28585  0fallfac  28586  binomfallfaclem1  28588  binomfallfaclem2  28589  binomrisefac  28591  fallfacval4  28592  predfz  28710  bpolycl  29241  bpolysum  29242  bpolydiflem  29243  fsumkthpow  29245  bpoly4  29248  mblfinlem2  29480  iblmulc2nc  29508  fdc  29692  irrapxlem1  30213  irrapxlem2  30214  irrapxlem3  30215  pellexlem5  30224  acongrep  30373  fzmaxdif  30374  acongeq  30376  jm2.22  30394  jm2.23  30395  jm2.26lem3  30400  jm2.26  30401  jm2.27dlem2  30409  fzssz  30862  monoords  30892  fmul01lt1lem1  30953  fmul01lt1lem2  30954  sumnnodd  30991  iblspltprt  31110  itgspltprt  31116  stoweidlem3  31122  stoweidlem11  31130  stoweidlem20  31139  stoweidlem26  31145  stoweidlem34  31153  stoweidlem59  31178  stirlinglem10  31202  dirkertrigeqlem1  31217  dirkertrigeqlem2  31218  dirkertrigeqlem3  31219  dirkertrigeq  31220  dirkeritg  31221  fourierdlem11  31237  fourierdlem12  31238  fourierdlem15  31241  fourierdlem34  31260  fourierdlem41  31267  fourierdlem46  31272  fourierdlem48  31274  fourierdlem49  31275  fourierdlem50  31276  fourierdlem54  31280  fourierdlem63  31289  fourierdlem64  31290  fourierdlem65  31291  fourierdlem79  31305  fourierdlem102  31328  fourierdlem103  31329  fourierdlem104  31330  fourierdlem114  31340  2elfz2melfz  31622  elfzelfzlble  31625  altgsumbc  31880  altgsumbcALT  31881
  Copyright terms: Public domain W3C validator