Theorem elfzelz 13485

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6511  (class class class)co 7387  ℤcz 12529  ℤ_≥cuz 12793  ...cfz 13468

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125

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 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-1st 7968  df-2nd 7969  df-neg 11408  df-z 12530  df-uz 12794  df-fz 13469

This theorem is referenced by:  elfzelzd  13486  fzssz  13487  elfz1eq  13496  fzsplit2  13510  fzdisj  13512  elfznn  13514  ssfzunsnext  13530  fznatpl1  13539  fzrev2i  13550  fzrev3i  13552  fznuz  13570  fzrevral  13573  fzshftral  13576  fznn0sub2  13596  elfzmlbm  13599  difelfznle  13603  predfz  13614  fzosplit  13653  sermono  13999  seqf1olem1  14006  seqf1olem2  14007  bcval2  14270  bcval4  14272  bccmpl  14274  bcp1nk  14282  bcval5  14283  bcpasc  14286  bccl2  14288  seqcoll2  14430  swrdval2  14611  swrdwrdsymb  14627  addlenrevpfx  14655  ccatpfx  14666  swrdswrd  14670  swrdpfx  14672  pfxccatin12lem2a  14692  pfxccatin12lem1  14693  swrdccatin2  14694  pfxccatin12lem2  14696  pfxccatin12  14698  spllen  14719  cshwidxm  14773  cshwidxn  14774  lswcshw  14780  2cshwcshw  14791  cshwcshid  14793  cshwcsh2id  14794  swrds2m  14907  seqshft  15051  sumrblem  15677  summolem2a  15681  fsum0diaglem  15742  mptfzshft  15744  fsumshftm  15747  fsum0diag2  15749  binomlem  15795  binom11  15798  bcxmas  15801  arisum  15826  geo2sum  15839  mertenslem1  15850  prodfn0  15860  prodrblem  15895  prodmolem2a  15900  fprodntriv  15908  fprodser  15915  fprodrev  15943  fallfacval3  15978  fallfacfwd  16002  0fallfac  16003  binomfallfaclem1  16005  binomfallfaclem2  16006  binomrisefac  16008  fallfacval4  16009  bpolycl  16018  bpolysum  16019  bpolydiflem  16020  fsumkthpow  16022  bpoly4  16025  fzm1ndvds  16292  pwp1fsum  16361  prmdvdsfz  16675  isprm7  16678  prmdvdsbc  16696  hashdvds  16745  phiprmpw  16746  prmdiveq  16756  modprminv  16770  modprminveq  16771  modprm0  16776  4sqlem11  16926  vdwapun  16945  prmop1  17009  prmdvdsprmo  17013  prmdvdsprmop  17014  prmgaplem1  17020  prmgaplem2  17021  prmgaplcmlem1  17022  prmgaplcmlem2  17023  prmgapprmo  17033  cshwshashlem1  17066  cshwshashlem2  17067  dfod2  19494  gsummptshft  19866  srgbinomlem3  20137  srgbinomlem4  20138  srgbinomlem  20139  freshmansdream  21484  chpscmatgsummon  22732  cayhamlem1  22753  iscmet3  25193  mbfi1fseqlem4  25619  itgz  25682  itgcl  25685  ibl0  25688  iblss  25706  iblss2  25707  itgss  25713  itgeqa  25715  iblconst  25719  iblabsr  25731  iblmulc2  25732  itgsplit  25737  dvfsumlem3  25935  plyeq0lem  26115  aalioulem1  26240  cxpeq  26667  birthdaylem2  26862  wilthlem1  26978  wilthlem3  26980  ftalem5  26987  basellem3  26993  basellem4  26994  dvdsppwf1o  27096  dvdsflf1o  27097  musum  27101  ppiub  27115  chtublem  27122  mersenne  27138  bposlem1  27195  lgsval2lem  27218  lgsdilem2  27244  lgsqrlem2  27258  gausslemma2dlem1a  27276  gausslemma2dlem1  27277  gausslemma2dlem3  27279  gausslemma2dlem4  27280  gausslemma2dlem5a  27281  gausslemma2dlem5  27282  gausslemma2dlem6  27283  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  2lgslem1a1  27300  2lgslem1a  27302  2lgslem1b  27303  rpvmasumlem  27398  dchrisumlem1  27400  dchrisumlem2  27401  dchrmusum2  27405  dchrvmasumlem1  27406  dchrvmasum2lem  27407  dchrvmasum2if  27408  dchrvmasumlem3  27410  dchrvmasumiflem1  27412  dchrvmasumiflem2  27413  dchrisum0flblem1  27419  rpvmasum2  27423  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrisum0lem3  27430  dchrmusumlem  27433  dchrvmasumlem  27434  logdivbnd  27467  pntpbnd1  27497  pntlemh  27510  pntlemf  27516  ostth2lem2  27545  axlowdimlem13  28881  axlowdimlem14  28882  axlowdimlem16  28884  crctcshlem4  29750  crctcshwlkn0  29751  erclwwlkeqlen  29948  clwwnisshclwwsn  29988  eleclclwwlknlem2  29990  erclwwlkneqlen  29997  fzm1ne1  32711  fzsplit3  32716  bcm1n  32718  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemodife  34489  ballotlemimin  34497  ballotlemsgt1  34502  ballotlemsel1i  34504  ballotlemsf1o  34505  ballotlemsi  34506  ballotlemsima  34507  ballotlemfg  34517  ballotlemfrc  34518  ballotlemfrcn0  34521  revpfxsfxrev  35103  swrdrevpfx  35104  pfxwlk  35111  swrdwlk  35114  erdszelem8  35185  erdszelem9  35186  cvmliftlem7  35278  supfz  35716  inffz  35717  bcprod  35725  fwddifnp1  36153  poimirlem1  37615  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem23  37637  poimirlem24  37638  poimirlem27  37641  poimirlem31  37645  poimirlem32  37646  mblfinlem2  37652  iblmulc2nc  37679  fdc  37739  lcmineqlem1  42017  lcmineqlem6  42022  lcmineqlem17  42033  aks4d1p1p1  42051  aks6d1c1  42104  hashscontpow  42110  aks6d1c5lem0  42123  aks6d1c5lem3  42125  aks6d1c5  42127  sticksstones6  42139  sticksstones7  42140  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  aks6d1c6lem1  42158  bcled  42166  bcle2d  42167  aks5lem5a  42179  grpods  42182  unitscyglem2  42184  unitscyglem4  42186  sumcubes  42301  irrapxlem1  42810  irrapxlem2  42811  irrapxlem3  42812  pellexlem5  42821  acongrep  42969  acongeq  42972  jm2.22  42984  jm2.23  42985  jm2.26lem3  42990  jm2.27dlem2  42999  hashnzfz  44309  monoords  45295  fmul01lt1lem1  45582  fmul01lt1lem2  45583  sumnnodd  45628  limsupubuzlem  45710  dvnmul  45941  dvnprodlem1  45944  dvnprodlem2  45945  iblsplit  45964  iblspltprt  45971  itgspltprt  45977  stoweidlem3  46001  stoweidlem11  46009  stoweidlem20  46018  stoweidlem26  46024  stoweidlem34  46032  stoweidlem59  46057  stirlinglem10  46081  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkeritg  46100  fourierdlem11  46116  fourierdlem12  46117  fourierdlem15  46120  fourierdlem34  46139  fourierdlem41  46146  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem54  46158  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem79  46183  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem114  46218  elaa2lem  46231  etransclem4  46236  etransclem7  46239  etransclem8  46240  etransclem17  46249  etransclem18  46250  etransclem20  46252  etransclem23  46255  etransclem27  46259  etransclem31  46263  etransclem32  46264  etransclem35  46267  etransclem41  46273  etransclem46  46278  etransclem48  46280  iundjiun  46458  caratheodorylem1  46524  2elfz2melfz  47319  elfzelfzlble  47322  el1fzopredsuc  47326  iccpartiltu  47423  iccpartgt  47428  iccpartnel  47439  fargshiftfo  47443  altgsumbc  48340  altgsumbcALT  48341  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609