Theorem elfzelz 13528

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

Syntax hints:   → wi 4   ∈ wcel 2099  ‘cfv 6543  (class class class)co 7415  ℤcz 12583  ℤ_≥cuz 12847  ...cfz 13511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5294  ax-nul 5301  ax-pr 5424  ax-un 7735  ax-cnex 11189  ax-resscn 11190

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-iun 4994  df-br 5144  df-opab 5206  df-mpt 5227  df-id 5571  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7418  df-oprab 7419  df-mpo 7420  df-1st 7988  df-2nd 7989  df-neg 11472  df-z 12584  df-uz 12848  df-fz 13512

This theorem is referenced by:  elfzelzd  13529  fzssz  13530  elfz1eq  13539  fzsplit2  13553  fzdisj  13555  elfznn  13557  ssfzunsnext  13573  fznatpl1  13582  fzrev2i  13593  fzrev3i  13595  fznuz  13610  fzrevral  13613  fzshftral  13616  fznn0sub2  13635  elfzmlbm  13638  difelfznle  13642  predfz  13653  fzosplit  13692  sermono  14026  seqf1olem1  14033  seqf1olem2  14034  bcval2  14291  bcval4  14293  bccmpl  14295  bcp1nk  14303  bcval5  14304  bcpasc  14307  bccl2  14309  seqcoll2  14453  swrdval2  14623  swrdwrdsymb  14639  addlenrevpfx  14667  ccatpfx  14678  swrdswrd  14682  swrdpfx  14684  pfxccatin12lem2a  14704  pfxccatin12lem1  14705  swrdccatin2  14706  pfxccatin12lem2  14708  pfxccatin12  14710  spllen  14731  cshwidxm  14785  cshwidxn  14786  lswcshw  14792  2cshwcshw  14803  cshwcshid  14805  cshwcsh2id  14806  swrds2m  14919  seqshft  15059  sumrblem  15684  summolem2a  15688  fsum0diaglem  15749  mptfzshft  15751  fsumshftm  15754  fsum0diag2  15756  binomlem  15802  binom11  15805  bcxmas  15808  arisum  15833  geo2sum  15846  mertenslem1  15857  prodfn0  15867  prodrblem  15900  prodmolem2a  15905  fprodntriv  15913  fprodser  15920  fprodrev  15948  fallfacval3  15983  fallfacfwd  16007  0fallfac  16008  binomfallfaclem1  16010  binomfallfaclem2  16011  binomrisefac  16013  fallfacval4  16014  bpolycl  16023  bpolysum  16024  bpolydiflem  16025  fsumkthpow  16027  bpoly4  16030  fzm1ndvds  16293  pwp1fsum  16362  prmdvdsfz  16670  isprm7  16673  prmdvdsbc  16692  hashdvds  16738  phiprmpw  16739  prmdiveq  16749  modprminv  16762  modprminveq  16763  modprm0  16768  4sqlem11  16918  vdwapun  16937  prmop1  17001  prmdvdsprmo  17005  prmdvdsprmop  17006  prmgaplem1  17012  prmgaplem2  17013  prmgaplcmlem1  17014  prmgaplcmlem2  17015  prmgapprmo  17025  cshwshashlem1  17059  cshwshashlem2  17060  dfod2  19513  gsummptshft  19885  srgbinomlem3  20162  srgbinomlem4  20163  srgbinomlem  20164  freshmansdream  21502  chpscmatgsummon  22741  cayhamlem1  22762  iscmet3  25215  mbfi1fseqlem4  25642  itgz  25704  itgcl  25707  ibl0  25710  iblss  25728  iblss2  25729  itgss  25735  itgeqa  25737  iblconst  25741  iblabsr  25753  iblmulc2  25754  itgsplit  25759  dvfsumlem3  25957  plyeq0lem  26138  aalioulem1  26261  cxpeq  26686  birthdaylem2  26878  wilthlem1  26994  wilthlem3  26996  ftalem5  27003  basellem3  27009  basellem4  27010  dvdsppwf1o  27112  dvdsflf1o  27113  musum  27117  ppiub  27131  chtublem  27138  mersenne  27154  bposlem1  27211  lgsval2lem  27234  lgsdilem2  27260  lgsqrlem2  27274  gausslemma2dlem1a  27292  gausslemma2dlem1  27293  gausslemma2dlem3  27295  gausslemma2dlem4  27296  gausslemma2dlem5a  27297  gausslemma2dlem5  27298  gausslemma2dlem6  27299  lgseisenlem1  27302  lgseisenlem2  27303  lgseisenlem3  27304  lgsquadlem1  27307  lgsquadlem2  27308  lgsquadlem3  27309  2lgslem1a1  27316  2lgslem1a  27318  2lgslem1b  27319  rpvmasumlem  27414  dchrisumlem1  27416  dchrisumlem2  27417  dchrmusum2  27421  dchrvmasumlem1  27422  dchrvmasum2lem  27423  dchrvmasum2if  27424  dchrvmasumlem3  27426  dchrvmasumiflem1  27428  dchrvmasumiflem2  27429  dchrisum0flblem1  27435  rpvmasum2  27439  dchrisum0lem1b  27442  dchrisum0lem1  27443  dchrisum0lem2a  27444  dchrisum0lem2  27445  dchrisum0lem3  27446  dchrmusumlem  27449  dchrvmasumlem  27450  logdivbnd  27483  pntpbnd1  27513  pntlemh  27526  pntlemf  27532  ostth2lem2  27561  axlowdimlem13  28759  axlowdimlem14  28760  axlowdimlem16  28762  crctcshlem4  29625  crctcshwlkn0  29626  erclwwlkeqlen  29823  clwwnisshclwwsn  29863  eleclclwwlknlem2  29865  erclwwlkneqlen  29872  fzm1ne1  32552  fzsplit3  32557  bcm1n  32558  ballotlemfc0  34107  ballotlemfcc  34108  ballotlemodife  34112  ballotlemimin  34120  ballotlemsgt1  34125  ballotlemsel1i  34127  ballotlemsf1o  34128  ballotlemsi  34129  ballotlemsima  34130  ballotlemfg  34140  ballotlemfrc  34141  ballotlemfrcn0  34144  revpfxsfxrev  34720  swrdrevpfx  34721  pfxwlk  34728  swrdwlk  34731  erdszelem8  34803  erdszelem9  34804  cvmliftlem7  34896  supfz  35318  inffz  35319  bcprod  35327  fwddifnp1  35756  poimirlem1  37089  poimirlem14  37102  poimirlem15  37103  poimirlem16  37104  poimirlem17  37105  poimirlem19  37107  poimirlem20  37108  poimirlem23  37111  poimirlem24  37112  poimirlem27  37115  poimirlem31  37119  poimirlem32  37120  mblfinlem2  37126  iblmulc2nc  37153  fdc  37213  lcmineqlem1  41495  lcmineqlem6  41500  lcmineqlem17  41511  aks4d1p1p1  41529  aks6d1c1  41582  hashscontpow  41588  aks6d1c5lem0  41601  aks6d1c5lem3  41603  aks6d1c5  41605  sticksstones6  41618  sticksstones7  41619  sticksstones10  41622  sticksstones12a  41624  sticksstones12  41625  aks6d1c6lem1  41637  bcled  41645  bcle2d  41646  metakunt15  41662  metakunt16  41663  metakunt19  41666  metakunt25  41672  metakunt33  41680  sumcubes  41864  irrapxlem1  42233  irrapxlem2  42234  irrapxlem3  42235  pellexlem5  42244  acongrep  42392  acongeq  42395  jm2.22  42407  jm2.23  42408  jm2.26lem3  42413  jm2.27dlem2  42422  hashnzfz  43748  monoords  44670  fmul01lt1lem1  44963  fmul01lt1lem2  44964  sumnnodd  45009  limsupubuzlem  45091  dvnmul  45322  dvnprodlem2  45326  iblsplit  45345  iblspltprt  45352  itgspltprt  45358  stoweidlem3  45382  stoweidlem11  45390  stoweidlem20  45399  stoweidlem26  45405  stoweidlem34  45413  stoweidlem59  45438  stirlinglem10  45462  dirkertrigeqlem1  45477  dirkertrigeqlem2  45478  dirkertrigeqlem3  45479  dirkertrigeq  45480  dirkeritg  45481  fourierdlem11  45497  fourierdlem12  45498  fourierdlem15  45501  fourierdlem34  45520  fourierdlem41  45527  fourierdlem46  45531  fourierdlem48  45533  fourierdlem49  45534  fourierdlem50  45535  fourierdlem54  45539  fourierdlem63  45548  fourierdlem64  45549  fourierdlem65  45550  fourierdlem79  45564  fourierdlem102  45587  fourierdlem103  45588  fourierdlem104  45589  fourierdlem114  45599  elaa2lem  45612  etransclem4  45617  etransclem7  45620  etransclem8  45621  etransclem17  45630  etransclem18  45631  etransclem20  45633  etransclem23  45636  etransclem27  45640  etransclem31  45644  etransclem32  45645  etransclem35  45648  etransclem41  45654  etransclem46  45659  etransclem48  45661  iundjiun  45839  caratheodorylem1  45905  2elfz2melfz  46689  elfzelfzlble  46692  el1fzopredsuc  46696  iccpartiltu  46753  iccpartgt  46758  iccpartnel  46769  fargshiftfo  46773  altgsumbc  47407  altgsumbcALT  47408  nn0sumshdiglemA  47683  nn0sumshdiglemB  47684