Theorem elfzelz 13446

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6486  (class class class)co 7353  ℤcz 12490  ℤ_≥cuz 12754  ...cfz 13429

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-resscn 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-1st 7931  df-2nd 7932  df-neg 11369  df-z 12491  df-uz 12755  df-fz 13430

This theorem is referenced by:  elfzelzd  13447  fzssz  13448  elfz1eq  13457  fzsplit2  13471  fzdisj  13473  elfznn  13475  ssfzunsnext  13491  fznatpl1  13500  fzrev2i  13511  fzrev3i  13513  fznuz  13531  fzrevral  13534  fzshftral  13537  fznn0sub2  13557  elfzmlbm  13560  difelfznle  13564  predfz  13575  fzosplit  13614  sermono  13960  seqf1olem1  13967  seqf1olem2  13968  bcval2  14231  bcval4  14233  bccmpl  14235  bcp1nk  14243  bcval5  14244  bcpasc  14247  bccl2  14249  seqcoll2  14391  swrdval2  14572  swrdwrdsymb  14588  ccatpfx  14626  swrdswrd  14630  swrdpfx  14632  pfxccatin12lem2a  14652  pfxccatin12lem1  14653  swrdccatin2  14654  pfxccatin12lem2  14656  pfxccatin12  14658  spllen  14679  cshwidxm  14733  cshwidxn  14734  lswcshw  14740  2cshwcshw  14751  cshwcshid  14753  cshwcsh2id  14754  swrds2m  14867  seqshft  15011  sumrblem  15637  summolem2a  15641  fsum0diaglem  15702  mptfzshft  15704  fsumshftm  15707  fsum0diag2  15709  binomlem  15755  binom11  15758  bcxmas  15761  arisum  15786  geo2sum  15799  mertenslem1  15810  prodfn0  15820  prodrblem  15855  prodmolem2a  15860  fprodntriv  15868  fprodser  15875  fprodrev  15903  fallfacval3  15938  fallfacfwd  15962  0fallfac  15963  binomfallfaclem1  15965  binomfallfaclem2  15966  binomrisefac  15968  fallfacval4  15969  bpolycl  15978  bpolysum  15979  bpolydiflem  15980  fsumkthpow  15982  bpoly4  15985  fzm1ndvds  16252  pwp1fsum  16321  prmdvdsfz  16635  isprm7  16638  prmdvdsbc  16656  hashdvds  16705  phiprmpw  16706  prmdiveq  16716  modprminv  16730  modprminveq  16731  modprm0  16736  4sqlem11  16886  vdwapun  16905  prmop1  16969  prmdvdsprmo  16973  prmdvdsprmop  16974  prmgaplem1  16980  prmgaplem2  16981  prmgaplcmlem1  16982  prmgaplcmlem2  16983  prmgapprmo  16993  cshwshashlem1  17026  cshwshashlem2  17027  dfod2  19462  gsummptshft  19834  srgbinomlem3  20132  srgbinomlem4  20133  srgbinomlem  20134  freshmansdream  21500  chpscmatgsummon  22749  cayhamlem1  22770  iscmet3  25210  mbfi1fseqlem4  25636  itgz  25699  itgcl  25702  ibl0  25705  iblss  25723  iblss2  25724  itgss  25730  itgeqa  25732  iblconst  25736  iblabsr  25748  iblmulc2  25749  itgsplit  25754  dvfsumlem3  25952  plyeq0lem  26132  aalioulem1  26257  cxpeq  26684  birthdaylem2  26879  wilthlem1  26995  wilthlem3  26997  ftalem5  27004  basellem3  27010  basellem4  27011  dvdsppwf1o  27113  dvdsflf1o  27114  musum  27118  ppiub  27132  chtublem  27139  mersenne  27155  bposlem1  27212  lgsval2lem  27235  lgsdilem2  27261  lgsqrlem2  27275  gausslemma2dlem1a  27293  gausslemma2dlem1  27294  gausslemma2dlem3  27296  gausslemma2dlem4  27297  gausslemma2dlem5a  27298  gausslemma2dlem5  27299  gausslemma2dlem6  27300  lgseisenlem1  27303  lgseisenlem2  27304  lgseisenlem3  27305  lgsquadlem1  27308  lgsquadlem2  27309  lgsquadlem3  27310  2lgslem1a1  27317  2lgslem1a  27319  2lgslem1b  27320  rpvmasumlem  27415  dchrisumlem1  27417  dchrisumlem2  27418  dchrmusum2  27422  dchrvmasumlem1  27423  dchrvmasum2lem  27424  dchrvmasum2if  27425  dchrvmasumlem3  27427  dchrvmasumiflem1  27429  dchrvmasumiflem2  27430  dchrisum0flblem1  27436  rpvmasum2  27440  dchrisum0lem1b  27443  dchrisum0lem1  27444  dchrisum0lem2a  27445  dchrisum0lem2  27446  dchrisum0lem3  27447  dchrmusumlem  27450  dchrvmasumlem  27451  logdivbnd  27484  pntpbnd1  27514  pntlemh  27527  pntlemf  27533  ostth2lem2  27562  axlowdimlem13  28918  axlowdimlem14  28919  axlowdimlem16  28921  crctcshlem4  29784  crctcshwlkn0  29785  erclwwlkeqlen  29982  clwwnisshclwwsn  30022  eleclclwwlknlem2  30024  erclwwlkneqlen  30031  fzm1ne1  32750  fzsplit3  32755  bcm1n  32757  ballotlemfc0  34480  ballotlemfcc  34481  ballotlemodife  34485  ballotlemimin  34493  ballotlemsgt1  34498  ballotlemsel1i  34500  ballotlemsf1o  34501  ballotlemsi  34502  ballotlemsima  34503  ballotlemfg  34513  ballotlemfrc  34514  ballotlemfrcn0  34517  revpfxsfxrev  35108  swrdrevpfx  35109  pfxwlk  35116  swrdwlk  35119  erdszelem8  35190  erdszelem9  35191  cvmliftlem7  35283  supfz  35721  inffz  35722  bcprod  35730  fwddifnp1  36158  poimirlem1  37620  poimirlem14  37633  poimirlem15  37634  poimirlem16  37635  poimirlem17  37636  poimirlem19  37638  poimirlem20  37639  poimirlem23  37642  poimirlem24  37643  poimirlem27  37646  poimirlem31  37650  poimirlem32  37651  mblfinlem2  37657  iblmulc2nc  37684  fdc  37744  lcmineqlem1  42022  lcmineqlem6  42027  lcmineqlem17  42038  aks4d1p1p1  42056  aks6d1c1  42109  hashscontpow  42115  aks6d1c5lem0  42128  aks6d1c5lem3  42130  aks6d1c5  42132  sticksstones6  42144  sticksstones7  42145  sticksstones10  42148  sticksstones12a  42150  sticksstones12  42151  aks6d1c6lem1  42163  bcled  42171  bcle2d  42172  aks5lem5a  42184  grpods  42187  unitscyglem2  42189  unitscyglem4  42191  sumcubes  42306  irrapxlem1  42815  irrapxlem2  42816  irrapxlem3  42817  pellexlem5  42826  acongrep  42973  acongeq  42976  jm2.22  42988  jm2.23  42989  jm2.26lem3  42994  jm2.27dlem2  43003  hashnzfz  44313  monoords  45299  fmul01lt1lem1  45585  fmul01lt1lem2  45586  sumnnodd  45631  limsupubuzlem  45713  dvnmul  45944  dvnprodlem1  45947  dvnprodlem2  45948  iblsplit  45967  iblspltprt  45974  itgspltprt  45980  stoweidlem3  46004  stoweidlem11  46012  stoweidlem20  46021  stoweidlem26  46027  stoweidlem34  46035  stoweidlem59  46060  stirlinglem10  46084  dirkertrigeqlem1  46099  dirkertrigeqlem2  46100  dirkertrigeqlem3  46101  dirkertrigeq  46102  dirkeritg  46103  fourierdlem11  46119  fourierdlem12  46120  fourierdlem15  46123  fourierdlem34  46142  fourierdlem41  46149  fourierdlem46  46153  fourierdlem48  46155  fourierdlem49  46156  fourierdlem50  46157  fourierdlem54  46161  fourierdlem63  46170  fourierdlem64  46171  fourierdlem65  46172  fourierdlem79  46186  fourierdlem102  46209  fourierdlem103  46210  fourierdlem104  46211  fourierdlem114  46221  elaa2lem  46234  etransclem4  46239  etransclem7  46242  etransclem8  46243  etransclem17  46252  etransclem18  46253  etransclem20  46255  etransclem23  46258  etransclem27  46262  etransclem31  46266  etransclem32  46267  etransclem35  46270  etransclem41  46276  etransclem46  46281  etransclem48  46283  iundjiun  46461  caratheodorylem1  46527  2elfz2melfz  47322  elfzelfzlble  47325  el1fzopredsuc  47329  iccpartiltu  47426  iccpartgt  47431  iccpartnel  47442  fargshiftfo  47446  altgsumbc  48356  altgsumbcALT  48357  nn0sumshdiglemA  48624  nn0sumshdiglemB  48625