Theorem elfzelz 13560

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

Syntax hints:   → wi 4   ∈ wcel 2105  ‘cfv 6562  (class class class)co 7430  ℤcz 12610  ℤ_≥cuz 12875  ...cfz 13543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8012  df-2nd 8013  df-neg 11492  df-z 12611  df-uz 12876  df-fz 13544

This theorem is referenced by:  elfzelzd  13561  fzssz  13562  elfz1eq  13571  fzsplit2  13585  fzdisj  13587  elfznn  13589  ssfzunsnext  13605  fznatpl1  13614  fzrev2i  13625  fzrev3i  13627  fznuz  13645  fzrevral  13648  fzshftral  13651  fznn0sub2  13671  elfzmlbm  13674  difelfznle  13678  predfz  13689  fzosplit  13728  sermono  14071  seqf1olem1  14078  seqf1olem2  14079  bcval2  14340  bcval4  14342  bccmpl  14344  bcp1nk  14352  bcval5  14353  bcpasc  14356  bccl2  14358  seqcoll2  14500  swrdval2  14680  swrdwrdsymb  14696  addlenrevpfx  14724  ccatpfx  14735  swrdswrd  14739  swrdpfx  14741  pfxccatin12lem2a  14761  pfxccatin12lem1  14762  swrdccatin2  14763  pfxccatin12lem2  14765  pfxccatin12  14767  spllen  14788  cshwidxm  14842  cshwidxn  14843  lswcshw  14849  2cshwcshw  14860  cshwcshid  14862  cshwcsh2id  14863  swrds2m  14976  seqshft  15120  sumrblem  15743  summolem2a  15747  fsum0diaglem  15808  mptfzshft  15810  fsumshftm  15813  fsum0diag2  15815  binomlem  15861  binom11  15864  bcxmas  15867  arisum  15892  geo2sum  15905  mertenslem1  15916  prodfn0  15926  prodrblem  15961  prodmolem2a  15966  fprodntriv  15974  fprodser  15981  fprodrev  16009  fallfacval3  16044  fallfacfwd  16068  0fallfac  16069  binomfallfaclem1  16071  binomfallfaclem2  16072  binomrisefac  16074  fallfacval4  16075  bpolycl  16084  bpolysum  16085  bpolydiflem  16086  fsumkthpow  16088  bpoly4  16091  fzm1ndvds  16355  pwp1fsum  16424  prmdvdsfz  16738  isprm7  16741  prmdvdsbc  16759  hashdvds  16808  phiprmpw  16809  prmdiveq  16819  modprminv  16832  modprminveq  16833  modprm0  16838  4sqlem11  16988  vdwapun  17007  prmop1  17071  prmdvdsprmo  17075  prmdvdsprmop  17076  prmgaplem1  17082  prmgaplem2  17083  prmgaplcmlem1  17084  prmgaplcmlem2  17085  prmgapprmo  17095  cshwshashlem1  17129  cshwshashlem2  17130  dfod2  19596  gsummptshft  19968  srgbinomlem3  20245  srgbinomlem4  20246  srgbinomlem  20247  freshmansdream  21610  chpscmatgsummon  22866  cayhamlem1  22887  iscmet3  25340  mbfi1fseqlem4  25767  itgz  25830  itgcl  25833  ibl0  25836  iblss  25854  iblss2  25855  itgss  25861  itgeqa  25863  iblconst  25867  iblabsr  25879  iblmulc2  25880  itgsplit  25885  dvfsumlem3  26083  plyeq0lem  26263  aalioulem1  26388  cxpeq  26814  birthdaylem2  27009  wilthlem1  27125  wilthlem3  27127  ftalem5  27134  basellem3  27140  basellem4  27141  dvdsppwf1o  27243  dvdsflf1o  27244  musum  27248  ppiub  27262  chtublem  27269  mersenne  27285  bposlem1  27342  lgsval2lem  27365  lgsdilem2  27391  lgsqrlem2  27405  gausslemma2dlem1a  27423  gausslemma2dlem1  27424  gausslemma2dlem3  27426  gausslemma2dlem4  27427  gausslemma2dlem5a  27428  gausslemma2dlem5  27429  gausslemma2dlem6  27430  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  2lgslem1a1  27447  2lgslem1a  27449  2lgslem1b  27450  rpvmasumlem  27545  dchrisumlem1  27547  dchrisumlem2  27548  dchrmusum2  27552  dchrvmasumlem1  27553  dchrvmasum2lem  27554  dchrvmasum2if  27555  dchrvmasumlem3  27557  dchrvmasumiflem1  27559  dchrvmasumiflem2  27560  dchrisum0flblem1  27566  rpvmasum2  27570  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0lem2  27576  dchrisum0lem3  27577  dchrmusumlem  27580  dchrvmasumlem  27581  logdivbnd  27614  pntpbnd1  27644  pntlemh  27657  pntlemf  27663  ostth2lem2  27692  axlowdimlem13  28983  axlowdimlem14  28984  axlowdimlem16  28986  crctcshlem4  29849  crctcshwlkn0  29850  erclwwlkeqlen  30047  clwwnisshclwwsn  30087  eleclclwwlknlem2  30089  erclwwlkneqlen  30096  fzm1ne1  32796  fzsplit3  32801  bcm1n  32802  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemodife  34478  ballotlemimin  34486  ballotlemsgt1  34491  ballotlemsel1i  34493  ballotlemsf1o  34494  ballotlemsi  34495  ballotlemsima  34496  ballotlemfg  34506  ballotlemfrc  34507  ballotlemfrcn0  34510  revpfxsfxrev  35099  swrdrevpfx  35100  pfxwlk  35107  swrdwlk  35110  erdszelem8  35182  erdszelem9  35183  cvmliftlem7  35275  supfz  35708  inffz  35709  bcprod  35717  fwddifnp1  36146  poimirlem1  37607  poimirlem14  37620  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem23  37629  poimirlem24  37630  poimirlem27  37633  poimirlem31  37637  poimirlem32  37638  mblfinlem2  37644  iblmulc2nc  37671  fdc  37731  lcmineqlem1  42010  lcmineqlem6  42015  lcmineqlem17  42026  aks4d1p1p1  42044  aks6d1c1  42097  hashscontpow  42103  aks6d1c5lem0  42116  aks6d1c5lem3  42118  aks6d1c5  42120  sticksstones6  42132  sticksstones7  42133  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem1  42151  bcled  42159  bcle2d  42160  aks5lem5a  42172  grpods  42175  unitscyglem2  42177  unitscyglem4  42179  metakunt15  42200  metakunt16  42201  metakunt19  42204  metakunt25  42210  metakunt33  42218  sumcubes  42325  irrapxlem1  42809  irrapxlem2  42810  irrapxlem3  42811  pellexlem5  42820  acongrep  42968  acongeq  42971  jm2.22  42983  jm2.23  42984  jm2.26lem3  42989  jm2.27dlem2  42998  hashnzfz  44315  monoords  45247  fmul01lt1lem1  45539  fmul01lt1lem2  45540  sumnnodd  45585  limsupubuzlem  45667  dvnmul  45898  dvnprodlem1  45901  dvnprodlem2  45902  iblsplit  45921  iblspltprt  45928  itgspltprt  45934  stoweidlem3  45958  stoweidlem11  45966  stoweidlem20  45975  stoweidlem26  45981  stoweidlem34  45989  stoweidlem59  46014  stirlinglem10  46038  dirkertrigeqlem1  46053  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkeritg  46057  fourierdlem11  46073  fourierdlem12  46074  fourierdlem15  46077  fourierdlem34  46096  fourierdlem41  46103  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem54  46115  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem79  46140  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem114  46175  elaa2lem  46188  etransclem4  46193  etransclem7  46196  etransclem8  46197  etransclem17  46206  etransclem18  46207  etransclem20  46209  etransclem23  46212  etransclem27  46216  etransclem31  46220  etransclem32  46221  etransclem35  46224  etransclem41  46230  etransclem46  46235  etransclem48  46237  iundjiun  46415  caratheodorylem1  46481  2elfz2melfz  47267  elfzelfzlble  47270  el1fzopredsuc  47274  iccpartiltu  47346  iccpartgt  47351  iccpartnel  47362  fargshiftfo  47366  altgsumbc  48196  altgsumbcALT  48197  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469