Theorem elfzelz 13185

Description: A member of a finite set of sequential integers is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzelz	⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

Proof of Theorem elfzelz

Step	Hyp	Ref	Expression
1		elfzuz 13181	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		eluzelz 12521	. 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ ℤ)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6418  (class class class)co 7255  ℤcz 12249  ℤ_≥cuz 12511  ...cfz 13168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-1st 7804  df-2nd 7805  df-neg 11138  df-z 12250  df-uz 12512  df-fz 13169

This theorem is referenced by:  elfzelzd  13186  fzssz  13187  elfz1eq  13196  fzsplit2  13210  fzdisj  13212  elfznn  13214  ssfzunsnext  13230  fznatpl1  13239  fzrev2i  13250  fzrev3i  13252  fznuz  13267  fzrevral  13270  fzshftral  13273  fznn0sub2  13292  elfzmlbm  13295  difelfznle  13299  predfz  13310  fzosplit  13348  sermono  13683  seqf1olem1  13690  seqf1olem2  13691  bcval2  13947  bcval4  13949  bccmpl  13951  bcp1nk  13959  bcval5  13960  bcpasc  13963  bccl2  13965  seqcoll2  14107  swrdval2  14287  swrdwrdsymb  14303  addlenrevpfx  14331  ccatpfx  14342  swrdswrd  14346  swrdpfx  14348  pfxccatin12lem2a  14368  pfxccatin12lem1  14369  swrdccatin2  14370  pfxccatin12lem2  14372  pfxccatin12  14374  spllen  14395  cshwidxm  14449  cshwidxn  14450  lswcshw  14456  2cshwcshw  14466  cshwcshid  14468  cshwcsh2id  14469  swrds2m  14582  seqshft  14724  sumrblem  15351  summolem2a  15355  fsum0diaglem  15416  mptfzshft  15418  fsumshftm  15421  fsum0diag2  15423  binomlem  15469  binom11  15472  bcxmas  15475  arisum  15500  geo2sum  15513  mertenslem1  15524  prodfn0  15534  prodrblem  15567  prodmolem2a  15572  fprodntriv  15580  fprodser  15587  fprodrev  15615  fallfacval3  15650  fallfacfwd  15674  0fallfac  15675  binomfallfaclem1  15677  binomfallfaclem2  15678  binomrisefac  15680  fallfacval4  15681  bpolycl  15690  bpolysum  15691  bpolydiflem  15692  fsumkthpow  15694  bpoly4  15697  fzm1ndvds  15959  pwp1fsum  16028  prmdvdsfz  16338  isprm7  16341  hashdvds  16404  phiprmpw  16405  prmdiveq  16415  modprminv  16428  modprminveq  16429  modprm0  16434  4sqlem11  16584  vdwapun  16603  prmop1  16667  prmdvdsprmo  16671  prmdvdsprmop  16672  prmgaplem1  16678  prmgaplem2  16679  prmgaplcmlem1  16680  prmgaplcmlem2  16681  prmgapprmo  16691  cshwshashlem1  16725  cshwshashlem2  16726  dfod2  19086  gsummptshft  19452  srgbinomlem3  19693  srgbinomlem4  19694  srgbinomlem  19695  chpscmatgsummon  21902  cayhamlem1  21923  iscmet3  24362  mbfi1fseqlem4  24788  itgz  24850  itgcl  24853  ibl0  24856  iblss  24874  iblss2  24875  itgss  24881  itgeqa  24883  iblconst  24887  iblabsr  24899  iblmulc2  24900  itgsplit  24905  dvfsumlem3  25097  plyeq0lem  25276  aalioulem1  25397  cxpeq  25815  birthdaylem2  26007  wilthlem1  26122  wilthlem3  26124  ftalem5  26131  basellem3  26137  basellem4  26138  dvdsppwf1o  26240  dvdsflf1o  26241  musum  26245  ppiub  26257  chtublem  26264  mersenne  26280  bposlem1  26337  lgsval2lem  26360  lgsdilem2  26386  lgsqrlem2  26400  gausslemma2dlem1a  26418  gausslemma2dlem1  26419  gausslemma2dlem3  26421  gausslemma2dlem4  26422  gausslemma2dlem5a  26423  gausslemma2dlem5  26424  gausslemma2dlem6  26425  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem3  26430  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  2lgslem1a1  26442  2lgslem1a  26444  2lgslem1b  26445  rpvmasumlem  26540  dchrisumlem1  26542  dchrisumlem2  26543  dchrmusum2  26547  dchrvmasumlem1  26548  dchrvmasum2lem  26549  dchrvmasum2if  26550  dchrvmasumlem3  26552  dchrvmasumiflem1  26554  dchrvmasumiflem2  26555  dchrisum0flblem1  26561  rpvmasum2  26565  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrisum0lem3  26572  dchrmusumlem  26575  dchrvmasumlem  26576  logdivbnd  26609  pntpbnd1  26639  pntlemh  26652  pntlemf  26658  ostth2lem2  26687  axlowdimlem13  27225  axlowdimlem14  27226  axlowdimlem16  27228  crctcshlem4  28086  crctcshwlkn0  28087  erclwwlkeqlen  28284  clwwnisshclwwsn  28324  eleclclwwlknlem2  28326  erclwwlkneqlen  28333  fzm1ne1  31012  fzsplit3  31017  bcm1n  31018  prmdvdsbc  31032  freshmansdream  31386  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemodife  32364  ballotlemimin  32372  ballotlemsgt1  32377  ballotlemsel1i  32379  ballotlemsf1o  32380  ballotlemsi  32381  ballotlemsima  32382  ballotlemfg  32392  ballotlemfrc  32393  ballotlemfrcn0  32396  revpfxsfxrev  32977  swrdrevpfx  32978  pfxwlk  32985  swrdwlk  32988  erdszelem8  33060  erdszelem9  33061  cvmliftlem7  33153  supfz  33600  inffz  33601  bcprod  33610  fwddifnp1  34394  poimirlem1  35705  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem23  35727  poimirlem24  35728  poimirlem27  35731  poimirlem31  35735  poimirlem32  35736  mblfinlem2  35742  iblmulc2nc  35769  fdc  35830  lcmineqlem1  39965  lcmineqlem6  39970  lcmineqlem17  39981  aks4d1p1p1  39999  sticksstones6  40035  sticksstones7  40036  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  metakunt15  40067  metakunt16  40068  metakunt19  40071  metakunt25  40077  metakunt33  40085  irrapxlem1  40560  irrapxlem2  40561  irrapxlem3  40562  pellexlem5  40571  acongrep  40718  acongeq  40721  jm2.22  40733  jm2.23  40734  jm2.26lem3  40739  jm2.27dlem2  40748  hashnzfz  41827  monoords  42726  fmul01lt1lem1  43015  fmul01lt1lem2  43016  sumnnodd  43061  limsupubuzlem  43143  dvnmul  43374  dvnprodlem2  43378  iblsplit  43397  iblspltprt  43404  itgspltprt  43410  stoweidlem3  43434  stoweidlem11  43442  stoweidlem20  43451  stoweidlem26  43457  stoweidlem34  43465  stoweidlem59  43490  stirlinglem10  43514  dirkertrigeqlem1  43529  dirkertrigeqlem2  43530  dirkertrigeqlem3  43531  dirkertrigeq  43532  dirkeritg  43533  fourierdlem11  43549  fourierdlem12  43550  fourierdlem15  43553  fourierdlem34  43572  fourierdlem41  43579  fourierdlem46  43583  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem54  43591  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem79  43616  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem114  43651  elaa2lem  43664  etransclem4  43669  etransclem7  43672  etransclem8  43673  etransclem17  43682  etransclem18  43683  etransclem20  43685  etransclem23  43688  etransclem27  43692  etransclem31  43696  etransclem32  43697  etransclem35  43700  etransclem41  43706  etransclem46  43711  etransclem48  43713  iundjiun  43888  caratheodorylem1  43954  2elfz2melfz  44698  elfzelfzlble  44701  el1fzopredsuc  44705  iccpartiltu  44762  iccpartgt  44767  iccpartnel  44778  fargshiftfo  44782  altgsumbc  45576  altgsumbcALT  45577  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854