Theorem elfzelz 13469

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

Syntax hints:   → wi 4   ∈ wcel 2119  ‘cfv 6485  (class class class)co 7356  ℤcz 12515  ℤ_≥cuz 12779  ...cfz 13452

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-neg 11371  df-z 12516  df-uz 12780  df-fz 13453

This theorem is referenced by:  elfzelzd  13470  fzssz  13471  elfz1eq  13480  fzsplit2  13494  fzdisj  13496  elfznn  13498  ssfzunsnext  13514  fznatpl1  13523  fzrev2i  13534  fzrev3i  13536  fznuz  13554  fzrevral  13557  fzshftral  13560  fznn0sub2  13580  elfzmlbm  13583  difelfznle  13587  predfz  13598  fzosplit  13638  sermono  13987  seqf1olem1  13994  seqf1olem2  13995  bcval2  14258  bcval4  14260  bccmpl  14262  bcp1nk  14270  bcval5  14271  bcpasc  14274  bccl2  14276  seqcoll2  14418  swrdval2  14600  swrdwrdsymb  14616  ccatpfx  14654  swrdswrd  14658  swrdpfx  14660  pfxccatin12lem2a  14680  pfxccatin12lem1  14681  swrdccatin2  14682  pfxccatin12lem2  14684  pfxccatin12  14686  spllen  14707  cshwidxm  14761  cshwidxn  14762  lswcshw  14768  2cshwcshw  14778  cshwcshid  14780  cshwcsh2id  14781  swrds2m  14894  seqshft  15038  sumrblem  15664  summolem2a  15668  fsum0diaglem  15729  mptfzshft  15731  fsumshftm  15734  fsum0diag2  15736  binomlem  15785  binom11  15788  bcxmas  15791  arisum  15816  geo2sum  15829  mertenslem1  15840  prodfn0  15850  prodrblem  15885  prodmolem2a  15890  fprodntriv  15898  fprodser  15905  fprodrev  15933  fallfacval3  15968  fallfacfwd  15992  0fallfac  15993  binomfallfaclem1  15995  binomfallfaclem2  15996  binomrisefac  15998  fallfacval4  15999  bpolycl  16008  bpolysum  16009  bpolydiflem  16010  fsumkthpow  16012  bpoly4  16015  fzm1ndvds  16282  pwp1fsum  16351  prmdvdsfz  16666  isprm7  16669  prmdvdsbc  16687  hashdvds  16736  phiprmpw  16737  prmdiveq  16747  modprminv  16761  modprminveq  16762  modprm0  16767  4sqlem11  16917  vdwapun  16936  prmop1  17000  prmdvdsprmo  17004  prmdvdsprmop  17005  prmgaplem1  17011  prmgaplem2  17012  prmgaplcmlem1  17013  prmgaplcmlem2  17014  prmgapprmo  17024  cshwshashlem1  17057  cshwshashlem2  17058  dfod2  19530  gsummptshft  19902  srgbinomlem3  20200  srgbinomlem4  20201  srgbinomlem  20202  freshmansdream  21549  chpscmatgsummon  22828  cayhamlem1  22849  iscmet3  25278  mbfi1fseqlem4  25703  itgz  25766  itgcl  25769  ibl0  25772  iblss  25790  iblss2  25791  itgss  25797  itgeqa  25799  iblconst  25803  iblabsr  25815  iblmulc2  25816  itgsplit  25821  dvfsumlem3  26013  plyeq0lem  26193  aalioulem1  26316  cxpeq  26739  birthdaylem2  26934  wilthlem1  27049  wilthlem3  27051  ftalem5  27058  basellem3  27064  basellem4  27065  dvdsppwf1o  27167  dvdsflf1o  27168  musum  27172  ppiub  27185  chtublem  27192  mersenne  27208  bposlem1  27265  lgsval2lem  27288  lgsdilem2  27314  lgsqrlem2  27328  gausslemma2dlem1a  27346  gausslemma2dlem1  27347  gausslemma2dlem3  27349  gausslemma2dlem4  27350  gausslemma2dlem5a  27351  gausslemma2dlem5  27352  gausslemma2dlem6  27353  lgseisenlem1  27356  lgseisenlem2  27357  lgseisenlem3  27358  lgsquadlem1  27361  lgsquadlem2  27362  lgsquadlem3  27363  2lgslem1a1  27370  2lgslem1a  27372  2lgslem1b  27373  rpvmasumlem  27468  dchrisumlem1  27470  dchrisumlem2  27471  dchrmusum2  27475  dchrvmasumlem1  27476  dchrvmasum2lem  27477  dchrvmasum2if  27478  dchrvmasumlem3  27480  dchrvmasumiflem1  27482  dchrvmasumiflem2  27483  dchrisum0flblem1  27489  rpvmasum2  27493  dchrisum0lem1b  27496  dchrisum0lem1  27497  dchrisum0lem2a  27498  dchrisum0lem2  27499  dchrisum0lem3  27500  dchrmusumlem  27503  dchrvmasumlem  27504  logdivbnd  27537  pntpbnd1  27567  pntlemh  27580  pntlemf  27586  ostth2lem2  27615  axlowdimlem13  29041  axlowdimlem14  29042  axlowdimlem16  29044  crctcshlem4  29906  crctcshwlkn0  29907  erclwwlkeqlen  30107  clwwnisshclwwsn  30147  eleclclwwlknlem2  30149  erclwwlkneqlen  30156  fzm1ne1  32880  fzsplit3  32885  bcm1n  32887  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemodife  34682  ballotlemimin  34690  ballotlemsgt1  34695  ballotlemsel1i  34697  ballotlemsf1o  34698  ballotlemsi  34699  ballotlemsima  34700  ballotlemfg  34710  ballotlemfrc  34711  ballotlemfrcn0  34714  revpfxsfxrev  35344  swrdrevpfx  35345  pfxwlk  35352  swrdwlk  35355  erdszelem8  35426  erdszelem9  35427  cvmliftlem7  35519  supfz  35957  inffz  35958  bcprod  35966  fwddifnp1  36393  poimirlem1  37988  poimirlem14  38001  poimirlem15  38002  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem23  38010  poimirlem24  38011  poimirlem27  38014  poimirlem31  38018  poimirlem32  38019  mblfinlem2  38025  iblmulc2nc  38052  fdc  38112  lcmineqlem1  42514  lcmineqlem6  42519  lcmineqlem17  42530  aks4d1p1p1  42548  aks6d1c1  42601  hashscontpow  42607  aks6d1c5lem0  42620  aks6d1c5lem3  42622  aks6d1c5  42624  sticksstones6  42636  sticksstones7  42637  sticksstones10  42640  sticksstones12a  42642  sticksstones12  42643  aks6d1c6lem1  42655  bcled  42663  bcle2d  42664  aks5lem5a  42676  grpods  42679  unitscyglem2  42681  unitscyglem4  42683  sumcubes  42790  irrapxlem1  43267  irrapxlem2  43268  irrapxlem3  43269  pellexlem5  43278  acongrep  43425  acongeq  43428  jm2.22  43440  jm2.23  43441  jm2.26lem3  43446  jm2.27dlem2  43455  hashnzfz  44764  monoords  45745  fmul01lt1lem1  46029  fmul01lt1lem2  46030  sumnnodd  46075  limsupubuzlem  46155  dvnmul  46386  dvnprodlem1  46389  dvnprodlem2  46390  iblsplit  46409  iblspltprt  46416  itgspltprt  46422  stoweidlem3  46446  stoweidlem11  46454  stoweidlem20  46463  stoweidlem26  46469  stoweidlem34  46477  stoweidlem59  46502  stirlinglem10  46526  dirkertrigeqlem1  46541  dirkertrigeqlem2  46542  dirkertrigeqlem3  46543  dirkertrigeq  46544  dirkeritg  46545  fourierdlem11  46561  fourierdlem12  46562  fourierdlem15  46565  fourierdlem34  46584  fourierdlem41  46591  fourierdlem46  46595  fourierdlem48  46597  fourierdlem49  46598  fourierdlem50  46599  fourierdlem54  46603  fourierdlem63  46612  fourierdlem64  46613  fourierdlem65  46614  fourierdlem79  46628  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem114  46663  elaa2lem  46676  etransclem4  46681  etransclem7  46684  etransclem8  46685  etransclem17  46694  etransclem18  46695  etransclem20  46697  etransclem23  46700  etransclem27  46704  etransclem31  46708  etransclem32  46709  etransclem35  46712  etransclem41  46718  etransclem46  46723  etransclem48  46725  iundjiun  46903  caratheodorylem1  46969  2elfz2melfz  47781  elfzelfzlble  47784  el1fzopredsuc  47789  iccpartiltu  47897  iccpartgt  47902  iccpartnel  47913  fargshiftfo  47917  altgsumbc  48843  altgsumbcALT  48844  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111