Theorem elfzelz 12911

Description: A member of a finite set of sequential integer 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 12907	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		eluzelz 12256	. 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ ℤ)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6357  (class class class)co 7158  ℤcz 11984  ℤ_≥cuz 12246  ...cfz 12895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-fv 6365  df-ov 7161  df-oprab 7162  df-mpo 7163  df-1st 7691  df-2nd 7692  df-neg 10875  df-z 11985  df-uz 12247  df-fz 12896

This theorem is referenced by:  fzssz  12912  elfz1eq  12921  fzsplit2  12935  fzdisj  12937  elfznn  12939  ssfzunsnext  12955  fznatpl1  12964  fzrev2i  12975  fzrev3i  12977  fznuz  12992  fzrevral  12995  fzshftral  12998  fznn0sub2  13017  elfzmlbm  13020  difelfznle  13024  predfz  13035  fzosplit  13073  sermono  13405  seqf1olem1  13412  seqf1olem2  13413  bcval2  13668  bcval4  13670  bccmpl  13672  bcp1nk  13680  bcval5  13681  bcpasc  13684  bccl2  13686  seqcoll  13825  seqcoll2  13826  swrdval2  14010  swrdwrdsymb  14026  ccatswrd  14032  addlenrevpfx  14054  ccatpfx  14065  swrdswrd  14069  swrdpfx  14071  pfxccatin12lem2a  14091  pfxccatin12lem1  14092  swrdccatin2  14093  pfxccatin12lem2  14095  pfxccatin12  14097  spllen  14118  splfv1  14119  cshwidxm  14172  cshwidxn  14173  lswcshw  14179  2cshwcshw  14189  cshwcshid  14191  cshwcsh2id  14192  swrds2m  14305  seqshft  14446  sumrblem  15070  summolem2a  15074  fsum0diaglem  15133  mptfzshft  15135  fsumrev  15136  fsumshftm  15138  fsum0diag2  15140  binomlem  15186  binom11  15189  bcxmas  15192  arisum  15217  geo2sum  15231  mertenslem1  15242  prodfn0  15252  prodrblem  15285  prodmolem2a  15290  fprodntriv  15298  fprodser  15305  fprod1p  15324  fprodrev  15333  fallfacval3  15368  fallfacfwd  15392  0fallfac  15393  binomfallfaclem1  15395  binomfallfaclem2  15396  binomrisefac  15398  fallfacval4  15399  bpolycl  15408  bpolysum  15409  bpolydiflem  15410  fsumkthpow  15412  bpoly4  15415  fzm1ndvds  15674  pwp1fsum  15744  prmdvdsfz  16051  isprm7  16054  hashdvds  16114  phiprmpw  16115  prmdiveq  16125  prmdivdiv  16126  modprminv  16138  modprminveq  16139  modprm0  16144  4sqlem11  16293  4sqlem12  16294  vdwapun  16312  prmop1  16376  prmdvdsprmo  16380  prmdvdsprmop  16381  prmgaplem1  16387  prmgaplem2  16388  prmgaplcmlem1  16389  prmgaplcmlem2  16390  prmgapprmo  16400  cshwshashlem1  16431  cshwshashlem2  16432  dfod2  18693  efgredleme  18871  efgredlemc  18873  efgredlemb  18874  gsummptshft  19058  srgbinomlem3  19294  srgbinomlem4  19295  srgbinomlem  19296  chpscmatgsummon  21455  cayhamlem1  21476  iscmet3  23898  mbfi1fseqlem4  24321  itgz  24383  itgcl  24386  ibl0  24389  iblss  24407  iblss2  24408  itgss  24414  itgeqa  24416  iblconst  24420  iblabsr  24432  iblmulc2  24433  itgsplit  24438  dvfsumlem3  24627  plyeq0lem  24802  aalioulem1  24923  cxpeq  25340  birthdaylem2  25532  wilthlem1  25647  wilthlem2  25648  wilthlem3  25649  ftalem5  25656  basellem3  25662  basellem4  25663  dvdsppwf1o  25765  dvdsflf1o  25766  musum  25770  ppiub  25782  chtublem  25789  mersenne  25805  bposlem1  25862  lgsval2lem  25885  lgsdilem2  25911  lgsqrlem2  25925  lgsqrlem4  25927  gausslemma2dlem1a  25943  gausslemma2dlem1  25944  gausslemma2dlem3  25946  gausslemma2dlem4  25947  gausslemma2dlem5a  25948  gausslemma2dlem5  25949  gausslemma2dlem6  25950  lgseisenlem1  25953  lgseisenlem2  25954  lgseisenlem3  25955  lgsquadlem1  25958  lgsquadlem2  25959  lgsquadlem3  25960  2lgslem1a1  25967  2lgslem1a  25969  2lgslem1b  25970  rpvmasumlem  26065  dchrisumlem1  26067  dchrisumlem2  26068  dchrmusum2  26072  dchrvmasumlem1  26073  dchrvmasum2lem  26074  dchrvmasum2if  26075  dchrvmasumlem3  26077  dchrvmasumiflem1  26079  dchrvmasumiflem2  26080  dchrisum0flblem1  26086  rpvmasum2  26090  dchrisum0lem1b  26093  dchrisum0lem1  26094  dchrisum0lem2a  26095  dchrisum0lem2  26096  dchrisum0lem3  26097  dchrmusumlem  26100  dchrvmasumlem  26101  logdivbnd  26134  pntpbnd1  26164  pntlemh  26177  pntlemj  26181  pntlemf  26183  ostth2lem2  26212  axlowdimlem13  26742  axlowdimlem14  26743  axlowdimlem16  26745  crctcshlem4  27600  crctcshwlkn0  27601  erclwwlkeqlen  27799  clwwnisshclwwsn  27840  eleclclwwlknlem2  27842  erclwwlkneqlen  27849  fzm1ne1  30514  fzsplit3  30519  bcm1n  30520  fzone1  30525  prmdvdsbc  30534  swrdf1  30632  cycpmco2lem7  30776  freshmansdream  30861  ballotlemfc0  31752  ballotlemfcc  31753  ballotlemodife  31757  ballotlemimin  31765  ballotlemsgt1  31770  ballotlemsel1i  31772  ballotlemsf1o  31773  ballotlemsi  31774  ballotlemsima  31775  ballotlemfg  31785  ballotlemfrc  31786  ballotlemfrceq  31788  ballotlemfrcn0  31789  ballotlemirc  31791  ballotlem1ri  31794  revpfxsfxrev  32364  swrdrevpfx  32365  pfxwlk  32372  swrdwlk  32375  erdszelem8  32447  erdszelem9  32448  cvmliftlem7  32540  supfz  32962  inffz  32963  bcprod  32972  fwddifnp1  33628  poimirlem1  34895  poimirlem2  34896  poimirlem7  34901  poimirlem14  34908  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem23  34917  poimirlem24  34918  poimirlem27  34921  poimirlem28  34922  poimirlem31  34925  poimirlem32  34926  mblfinlem2  34932  iblmulc2nc  34959  fdc  35022  irrapxlem1  39426  irrapxlem2  39427  irrapxlem3  39428  pellexlem5  39437  acongrep  39584  fzmaxdif  39585  acongeq  39587  jm2.22  39599  jm2.23  39600  jm2.26lem3  39605  jm2.26  39606  jm2.27dlem2  39614  hashnzfz  40659  monoords  41571  elfzelzd  41589  fmul01lt1lem1  41872  fmul01lt1lem2  41873  sumnnodd  41918  limsupubuzlem  42000  dvnmul  42235  dvnprodlem2  42239  iblsplit  42258  iblspltprt  42265  itgspltprt  42271  stoweidlem3  42295  stoweidlem11  42303  stoweidlem20  42312  stoweidlem26  42318  stoweidlem34  42326  stoweidlem59  42351  stirlinglem10  42375  dirkertrigeqlem1  42390  dirkertrigeqlem2  42391  dirkertrigeqlem3  42392  dirkertrigeq  42393  dirkeritg  42394  fourierdlem11  42410  fourierdlem12  42411  fourierdlem15  42414  fourierdlem34  42433  fourierdlem41  42440  fourierdlem46  42444  fourierdlem48  42446  fourierdlem49  42447  fourierdlem50  42448  fourierdlem54  42452  fourierdlem63  42461  fourierdlem64  42462  fourierdlem65  42463  fourierdlem79  42477  fourierdlem102  42500  fourierdlem103  42501  fourierdlem104  42502  fourierdlem114  42512  elaa2lem  42525  etransclem4  42530  etransclem7  42533  etransclem8  42534  etransclem17  42543  etransclem18  42544  etransclem20  42546  etransclem23  42549  etransclem27  42553  etransclem31  42557  etransclem32  42558  etransclem35  42561  etransclem41  42567  etransclem46  42572  etransclem48  42574  iundjiun  42749  caratheodorylem1  42815  2elfz2melfz  43525  elfzelfzlble  43528  el1fzopredsuc  43532  iccpartgtprec  43587  iccpartiltu  43589  iccpartgt  43594  iccpartnel  43605  fargshiftfo  43609  altgsumbc  44407  altgsumbcALT  44408  nn0sumshdiglemA  44686  nn0sumshdiglemB  44687