Theorem elfzelz 13564

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 13560	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		eluzelz 12888	. 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ ℤ)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6561  (class class class)co 7431  ℤcz 12613  ℤ_≥cuz 12878  ...cfz 13547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-neg 11495  df-z 12614  df-uz 12879  df-fz 13548

This theorem is referenced by:  elfzelzd  13565  fzssz  13566  elfz1eq  13575  fzsplit2  13589  fzdisj  13591  elfznn  13593  ssfzunsnext  13609  fznatpl1  13618  fzrev2i  13629  fzrev3i  13631  fznuz  13649  fzrevral  13652  fzshftral  13655  fznn0sub2  13675  elfzmlbm  13678  difelfznle  13682  predfz  13693  fzosplit  13732  sermono  14075  seqf1olem1  14082  seqf1olem2  14083  bcval2  14344  bcval4  14346  bccmpl  14348  bcp1nk  14356  bcval5  14357  bcpasc  14360  bccl2  14362  seqcoll2  14504  swrdval2  14684  swrdwrdsymb  14700  addlenrevpfx  14728  ccatpfx  14739  swrdswrd  14743  swrdpfx  14745  pfxccatin12lem2a  14765  pfxccatin12lem1  14766  swrdccatin2  14767  pfxccatin12lem2  14769  pfxccatin12  14771  spllen  14792  cshwidxm  14846  cshwidxn  14847  lswcshw  14853  2cshwcshw  14864  cshwcshid  14866  cshwcsh2id  14867  swrds2m  14980  seqshft  15124  sumrblem  15747  summolem2a  15751  fsum0diaglem  15812  mptfzshft  15814  fsumshftm  15817  fsum0diag2  15819  binomlem  15865  binom11  15868  bcxmas  15871  arisum  15896  geo2sum  15909  mertenslem1  15920  prodfn0  15930  prodrblem  15965  prodmolem2a  15970  fprodntriv  15978  fprodser  15985  fprodrev  16013  fallfacval3  16048  fallfacfwd  16072  0fallfac  16073  binomfallfaclem1  16075  binomfallfaclem2  16076  binomrisefac  16078  fallfacval4  16079  bpolycl  16088  bpolysum  16089  bpolydiflem  16090  fsumkthpow  16092  bpoly4  16095  fzm1ndvds  16359  pwp1fsum  16428  prmdvdsfz  16742  isprm7  16745  prmdvdsbc  16763  hashdvds  16812  phiprmpw  16813  prmdiveq  16823  modprminv  16837  modprminveq  16838  modprm0  16843  4sqlem11  16993  vdwapun  17012  prmop1  17076  prmdvdsprmo  17080  prmdvdsprmop  17081  prmgaplem1  17087  prmgaplem2  17088  prmgaplcmlem1  17089  prmgaplcmlem2  17090  prmgapprmo  17100  cshwshashlem1  17133  cshwshashlem2  17134  dfod2  19582  gsummptshft  19954  srgbinomlem3  20225  srgbinomlem4  20226  srgbinomlem  20227  freshmansdream  21593  chpscmatgsummon  22851  cayhamlem1  22872  iscmet3  25327  mbfi1fseqlem4  25753  itgz  25816  itgcl  25819  ibl0  25822  iblss  25840  iblss2  25841  itgss  25847  itgeqa  25849  iblconst  25853  iblabsr  25865  iblmulc2  25866  itgsplit  25871  dvfsumlem3  26069  plyeq0lem  26249  aalioulem1  26374  cxpeq  26800  birthdaylem2  26995  wilthlem1  27111  wilthlem3  27113  ftalem5  27120  basellem3  27126  basellem4  27127  dvdsppwf1o  27229  dvdsflf1o  27230  musum  27234  ppiub  27248  chtublem  27255  mersenne  27271  bposlem1  27328  lgsval2lem  27351  lgsdilem2  27377  lgsqrlem2  27391  gausslemma2dlem1a  27409  gausslemma2dlem1  27410  gausslemma2dlem3  27412  gausslemma2dlem4  27413  gausslemma2dlem5a  27414  gausslemma2dlem5  27415  gausslemma2dlem6  27416  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  2lgslem1a1  27433  2lgslem1a  27435  2lgslem1b  27436  rpvmasumlem  27531  dchrisumlem1  27533  dchrisumlem2  27534  dchrmusum2  27538  dchrvmasumlem1  27539  dchrvmasum2lem  27540  dchrvmasum2if  27541  dchrvmasumlem3  27543  dchrvmasumiflem1  27545  dchrvmasumiflem2  27546  dchrisum0flblem1  27552  rpvmasum2  27556  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2a  27561  dchrisum0lem2  27562  dchrisum0lem3  27563  dchrmusumlem  27566  dchrvmasumlem  27567  logdivbnd  27600  pntpbnd1  27630  pntlemh  27643  pntlemf  27649  ostth2lem2  27678  axlowdimlem13  28969  axlowdimlem14  28970  axlowdimlem16  28972  crctcshlem4  29840  crctcshwlkn0  29841  erclwwlkeqlen  30038  clwwnisshclwwsn  30078  eleclclwwlknlem2  30080  erclwwlkneqlen  30087  fzm1ne1  32790  fzsplit3  32795  bcm1n  32797  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemodife  34500  ballotlemimin  34508  ballotlemsgt1  34513  ballotlemsel1i  34515  ballotlemsf1o  34516  ballotlemsi  34517  ballotlemsima  34518  ballotlemfg  34528  ballotlemfrc  34529  ballotlemfrcn0  34532  revpfxsfxrev  35121  swrdrevpfx  35122  pfxwlk  35129  swrdwlk  35132  erdszelem8  35203  erdszelem9  35204  cvmliftlem7  35296  supfz  35729  inffz  35730  bcprod  35738  fwddifnp1  36166  poimirlem1  37628  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem23  37650  poimirlem24  37651  poimirlem27  37654  poimirlem31  37658  poimirlem32  37659  mblfinlem2  37665  iblmulc2nc  37692  fdc  37752  lcmineqlem1  42030  lcmineqlem6  42035  lcmineqlem17  42046  aks4d1p1p1  42064  aks6d1c1  42117  hashscontpow  42123  aks6d1c5lem0  42136  aks6d1c5lem3  42138  aks6d1c5  42140  sticksstones6  42152  sticksstones7  42153  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  aks6d1c6lem1  42171  bcled  42179  bcle2d  42180  aks5lem5a  42192  grpods  42195  unitscyglem2  42197  unitscyglem4  42199  metakunt15  42220  metakunt16  42221  metakunt19  42224  metakunt25  42230  metakunt33  42238  sumcubes  42347  irrapxlem1  42833  irrapxlem2  42834  irrapxlem3  42835  pellexlem5  42844  acongrep  42992  acongeq  42995  jm2.22  43007  jm2.23  43008  jm2.26lem3  43013  jm2.27dlem2  43022  hashnzfz  44339  monoords  45309  fmul01lt1lem1  45599  fmul01lt1lem2  45600  sumnnodd  45645  limsupubuzlem  45727  dvnmul  45958  dvnprodlem1  45961  dvnprodlem2  45962  iblsplit  45981  iblspltprt  45988  itgspltprt  45994  stoweidlem3  46018  stoweidlem11  46026  stoweidlem20  46035  stoweidlem26  46041  stoweidlem34  46049  stoweidlem59  46074  stirlinglem10  46098  dirkertrigeqlem1  46113  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkeritg  46117  fourierdlem11  46133  fourierdlem12  46134  fourierdlem15  46137  fourierdlem34  46156  fourierdlem41  46163  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem54  46175  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem79  46200  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem114  46235  elaa2lem  46248  etransclem4  46253  etransclem7  46256  etransclem8  46257  etransclem17  46266  etransclem18  46267  etransclem20  46269  etransclem23  46272  etransclem27  46276  etransclem31  46280  etransclem32  46281  etransclem35  46284  etransclem41  46290  etransclem46  46295  etransclem48  46297  iundjiun  46475  caratheodorylem1  46541  2elfz2melfz  47330  elfzelfzlble  47333  el1fzopredsuc  47337  iccpartiltu  47409  iccpartgt  47414  iccpartnel  47425  fargshiftfo  47429  altgsumbc  48268  altgsumbcALT  48269  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541