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 2114  ‘cfv 6492  (class class class)co 7360  ℤ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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  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  21564  chpscmatgsummon  22820  cayhamlem1  22841  iscmet3  25270  mbfi1fseqlem4  25695  itgz  25758  itgcl  25761  ibl0  25764  iblss  25782  iblss2  25783  itgss  25789  itgeqa  25791  iblconst  25795  iblabsr  25807  iblmulc2  25808  itgsplit  25813  dvfsumlem3  26005  plyeq0lem  26185  aalioulem1  26309  cxpeq  26734  birthdaylem2  26929  wilthlem1  27045  wilthlem3  27047  ftalem5  27054  basellem3  27060  basellem4  27061  dvdsppwf1o  27163  dvdsflf1o  27164  musum  27168  ppiub  27181  chtublem  27188  mersenne  27204  bposlem1  27261  lgsval2lem  27284  lgsdilem2  27310  lgsqrlem2  27324  gausslemma2dlem1a  27342  gausslemma2dlem1  27343  gausslemma2dlem3  27345  gausslemma2dlem4  27346  gausslemma2dlem5a  27347  gausslemma2dlem5  27348  gausslemma2dlem6  27349  lgseisenlem1  27352  lgseisenlem2  27353  lgseisenlem3  27354  lgsquadlem1  27357  lgsquadlem2  27358  lgsquadlem3  27359  2lgslem1a1  27366  2lgslem1a  27368  2lgslem1b  27369  rpvmasumlem  27464  dchrisumlem1  27466  dchrisumlem2  27467  dchrmusum2  27471  dchrvmasumlem1  27472  dchrvmasum2lem  27473  dchrvmasum2if  27474  dchrvmasumlem3  27476  dchrvmasumiflem1  27478  dchrvmasumiflem2  27479  dchrisum0flblem1  27485  rpvmasum2  27489  dchrisum0lem1b  27492  dchrisum0lem1  27493  dchrisum0lem2a  27494  dchrisum0lem2  27495  dchrisum0lem3  27496  dchrmusumlem  27499  dchrvmasumlem  27500  logdivbnd  27533  pntpbnd1  27563  pntlemh  27576  pntlemf  27582  ostth2lem2  27611  axlowdimlem13  29037  axlowdimlem14  29038  axlowdimlem16  29040  crctcshlem4  29903  crctcshwlkn0  29904  erclwwlkeqlen  30104  clwwnisshclwwsn  30144  eleclclwwlknlem2  30146  erclwwlkneqlen  30153  fzm1ne1  32876  fzsplit3  32881  bcm1n  32883  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemodife  34658  ballotlemimin  34666  ballotlemsgt1  34671  ballotlemsel1i  34673  ballotlemsf1o  34674  ballotlemsi  34675  ballotlemsima  34676  ballotlemfg  34686  ballotlemfrc  34687  ballotlemfrcn0  34690  revpfxsfxrev  35314  swrdrevpfx  35315  pfxwlk  35322  swrdwlk  35325  erdszelem8  35396  erdszelem9  35397  cvmliftlem7  35489  supfz  35927  inffz  35928  bcprod  35936  fwddifnp1  36363  poimirlem1  37956  poimirlem14  37969  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem23  37978  poimirlem24  37979  poimirlem27  37982  poimirlem31  37986  poimirlem32  37987  mblfinlem2  37993  iblmulc2nc  38020  fdc  38080  lcmineqlem1  42482  lcmineqlem6  42487  lcmineqlem17  42498  aks4d1p1p1  42516  aks6d1c1  42569  hashscontpow  42575  aks6d1c5lem0  42588  aks6d1c5lem3  42590  aks6d1c5  42592  sticksstones6  42604  sticksstones7  42605  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  aks6d1c6lem1  42623  bcled  42631  bcle2d  42632  aks5lem5a  42644  grpods  42647  unitscyglem2  42649  unitscyglem4  42651  sumcubes  42759  irrapxlem1  43268  irrapxlem2  43269  irrapxlem3  43270  pellexlem5  43279  acongrep  43426  acongeq  43429  jm2.22  43441  jm2.23  43442  jm2.26lem3  43447  jm2.27dlem2  43456  hashnzfz  44765  monoords  45748  fmul01lt1lem1  46032  fmul01lt1lem2  46033  sumnnodd  46078  limsupubuzlem  46158  dvnmul  46389  dvnprodlem1  46392  dvnprodlem2  46393  iblsplit  46412  iblspltprt  46419  itgspltprt  46425  stoweidlem3  46449  stoweidlem11  46457  stoweidlem20  46466  stoweidlem26  46472  stoweidlem34  46480  stoweidlem59  46505  stirlinglem10  46529  dirkertrigeqlem1  46544  dirkertrigeqlem2  46545  dirkertrigeqlem3  46546  dirkertrigeq  46547  dirkeritg  46548  fourierdlem11  46564  fourierdlem12  46565  fourierdlem15  46568  fourierdlem34  46587  fourierdlem41  46594  fourierdlem46  46598  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem54  46606  fourierdlem63  46615  fourierdlem64  46616  fourierdlem65  46617  fourierdlem79  46631  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem114  46666  elaa2lem  46679  etransclem4  46684  etransclem7  46687  etransclem8  46688  etransclem17  46697  etransclem18  46698  etransclem20  46700  etransclem23  46703  etransclem27  46707  etransclem31  46711  etransclem32  46712  etransclem35  46715  etransclem41  46721  etransclem46  46726  etransclem48  46728  iundjiun  46906  caratheodorylem1  46972  2elfz2melfz  47778  elfzelfzlble  47781  el1fzopredsuc  47786  iccpartiltu  47894  iccpartgt  47899  iccpartnel  47910  fargshiftfo  47914  altgsumbc  48840  altgsumbcALT  48841  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108