Theorem elfzelz 13649

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6537  (class class class)co 7418  ℤcz 12686  ℤ_≥cuz 12958  ...cfz 13632

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7421  df-oprab 7422  df-mpo 7423  df-1st 7999  df-2nd 8000  df-neg 11537  df-z 12687  df-uz 12959  df-fz 13633

This theorem is used by:  elfzelzd  13650  fzssz  13651  elfz1eq  13661  fzsplit2  13676  fzdisj  13678  elfznn  13680  ssfzunsnext  13696  fznatpl1  13705  fzrev2i  13716  fzrev3i  13718  fznuz  13736  fzrevral  13739  fzshftral  13742  fznn0sub2  13762  elfzmlbm  13765  difelfznle  13769  predfz  13780  fzosplit  13820  sermono  14170  seqf1olem1  14177  seqf1olem2  14178  bcval2  14442  bcval4  14444  bccmpl  14446  bcp1nk  14454  bcval5  14455  bcpasc  14458  bccl2  14460  seqcoll2  14603  swrdval2  14787  swrdwrdsymb  14805  ccatpfx  14843  swrdswrd  14847  swrdpfx  14849  pfxccatin12lem2a  14869  pfxccatin12lem1  14870  swrdccatin2  14871  pfxccatin12lem2  14873  pfxccatin12  14875  spllen  14896  revpfxsfxrev  14910  swrdrevpfx  14911  cshwidxm  14952  cshwidxn  14953  lswcshw  14959  2cshwcshw  14969  cshwcshid  14971  cshwcsh2id  14972  swrds2m  15085  seqshft  15231  sumrblem  15870  summolem2a  15874  fsum0diaglem  15935  mptfzshft  15937  fsumshftm  15940  fsum0diag2  15942  binomlem  15991  binom11  15994  bcxmas  15997  arisum  16022  geo2sum  16035  mertenslem1  16046  prodfn0  16056  prodrblem  16089  prodmolem2a  16094  fprodntriv  16102  fprodser  16109  fprodrev  16137  fallfacval3  16172  fallfacfwd  16195  0fallfac  16196  binomfallfaclem1  16198  binomfallfaclem2  16199  binomrisefac  16201  fallfacval4  16202  bpolycl  16211  bpolysum  16212  bpolydiflem  16213  fsumkthpow  16215  bpoly4  16218  fzm1ndvds  16485  pwp1fsum  16554  prmdvdsfz  16874  isprm7  16877  prmdvdsbc  16895  hashdvds  16945  phiprmpw  16946  prmdiveq  16956  modprminv  16970  modprminveq  16971  modprm0  16976  4sqlem11  17126  vdwapun  17145  prmop1  17209  prmdvdsprmo  17213  prmdvdsprmop  17214  prmgaplem1  17220  prmgaplem2  17221  prmgaplcmlem1  17222  prmgaplcmlem2  17223  prmgapprmo  17233  cshwshashlem1  17266  cshwshashlem2  17267  dfod2  19771  gsummptshft  20143  srgbinomlem3  20447  srgbinomlem4  20448  srgbinomlem  20449  freshmansdream  21873  chpscmatgsummon  23156  cayhamlem1  23177  iscmet3  25607  mbfi1fseqlem4  26032  itgz  26094  itgcl  26097  ibl0  26100  iblss  26118  iblss2  26119  itgss  26125  itgeqa  26127  iblconst  26131  iblabsr  26143  iblmulc2  26144  itgsplit  26149  dvfsumlem3  26341  plyeq0lem  26522  aalioulem1  26652  cxpeq  27078  birthdaylem2  27273  wilthlem1  27388  wilthlem3  27390  ftalem5  27397  basellem3  27403  basellem4  27404  dvdsppwf1o  27506  dvdsflf1o  27507  musum  27511  ppiub  27524  chtublem  27531  mersenne  27547  bposlem1  27604  lgsval2lem  27627  lgsdilem2  27653  lgsqrlem2  27667  gausslemma2dlem1a  27685  gausslemma2dlem1  27686  gausslemma2dlem3  27688  gausslemma2dlem4  27689  gausslemma2dlem5a  27690  gausslemma2dlem5  27691  gausslemma2dlem6  27692  lgseisenlem1  27695  lgseisenlem2  27696  lgseisenlem3  27697  lgsquadlem1  27700  lgsquadlem2  27701  lgsquadlem3  27702  2lgslem1a1  27709  2lgslem1a  27711  2lgslem1b  27712  rpvmasumlem  27807  dchrisumlem1  27809  dchrisumlem2  27810  dchrmusum2  27814  dchrvmasumlem1  27815  dchrvmasum2lem  27816  dchrvmasum2if  27817  dchrvmasumlem3  27819  dchrvmasumiflem1  27821  dchrvmasumiflem2  27822  dchrisum0flblem1  27828  rpvmasum2  27832  dchrisum0lem1b  27835  dchrisum0lem1  27836  dchrisum0lem2a  27837  dchrisum0lem2  27838  dchrisum0lem3  27839  dchrmusumlem  27842  dchrvmasumlem  27843  logdivbnd  27876  pntpbnd1  27906  pntlemh  27919  pntlemf  27925  ostth2lem2  27954  axlowdimlem13  29525  axlowdimlem14  29526  axlowdimlem16  29528  pfxwlk  30259  swrdwlk  30261  crctcshlem4  30402  crctcshwlkn0  30403  erclwwlkeqlen  30603  clwwnisshclwwsn  30643  eleclclwwlknlem2  30645  erclwwlkneqlen  30652  fzm1ne1  33373  fzsplit3  33378  bcm1n  33380  ballotlemfc0  35118  ballotlemfcc  35119  ballotlemodife  35123  ballotlemimin  35131  ballotlemsgt1  35136  ballotlemsel1i  35138  ballotlemsf1o  35139  ballotlemsi  35140  ballotlemsima  35141  ballotlemfg  35151  ballotlemfrc  35152  ballotlemfrcn0  35155  erdszelem8  35942  erdszelem9  35943  cvmliftlem7  36035  supfz  36473  inffz  36474  bcprod  36482  fwddifnp1  36910  poimirlem1  38519  poimirlem14  38532  poimirlem15  38533  poimirlem16  38534  poimirlem17  38535  poimirlem19  38537  poimirlem20  38538  poimirlem23  38541  poimirlem24  38542  poimirlem27  38545  poimirlem31  38549  poimirlem32  38550  mblfinlem2  38556  iblmulc2nc  38583  fdc  38659  lcmineqlem1  43059  lcmineqlem6  43064  lcmineqlem17  43075  aks4d1p1p1  43093  aks6d1c1  43146  hashscontpow  43152  aks6d1c5lem0  43165  aks6d1c5lem3  43167  aks6d1c5  43169  sticksstones6  43181  sticksstones7  43182  sticksstones10  43185  sticksstones12a  43187  sticksstones12  43188  aks6d1c6lem1  43200  bcled  43208  bcle2d  43209  aks5lem5a  43221  grpods  43224  unitscyglem2  43226  unitscyglem4  43228  sumcubes  43350  irrapxlem1  43808  irrapxlem2  43809  irrapxlem3  43810  pellexlem5  43819  acongrep  43966  acongeq  43969  jm2.22  43981  jm2.23  43982  jm2.26lem3  43987  jm2.27dlem2  43996  hashnzfz  45289  monoords  46282  fmul01lt1lem1  46565  fmul01lt1lem2  46566  sumnnodd  46611  limsupubuzlem  46691  dvnmul  46922  dvnprodlem1  46925  dvnprodlem2  46926  iblsplit  46945  iblspltprt  46952  itgspltprt  46958  stoweidlem3  46982  stoweidlem11  46990  stoweidlem20  46999  stoweidlem26  47005  stoweidlem34  47013  stoweidlem59  47038  stirlinglem10  47062  dirkertrigeqlem1  47077  dirkertrigeqlem2  47078  dirkertrigeqlem3  47079  dirkertrigeq  47080  dirkeritg  47081  fourierdlem11  47097  fourierdlem12  47098  fourierdlem15  47101  fourierdlem34  47120  fourierdlem41  47127  fourierdlem46  47131  fourierdlem48  47133  fourierdlem49  47134  fourierdlem50  47135  fourierdlem54  47139  fourierdlem63  47148  fourierdlem64  47149  fourierdlem65  47150  fourierdlem79  47164  fourierdlem102  47187  fourierdlem103  47188  fourierdlem104  47189  fourierdlem114  47199  elaa2lem  47212  etransclem4  47217  etransclem7  47220  etransclem8  47221  etransclem17  47230  etransclem18  47231  etransclem20  47233  etransclem23  47236  etransclem27  47240  etransclem31  47244  etransclem32  47245  etransclem35  47248  etransclem41  47254  etransclem46  47259  etransclem48  47261  iundjiun  47439  caratheodorylem1  47505  2elfz2melfz  48357  elfzelfzlble  48360  el1fzopredsuc  48365  iccpartiltu  48473  iccpartgt  48478  iccpartnel  48489  fargshiftfo  48493  altgsumbc  49433  altgsumbcALT  49434  nn0sumshdiglemA  49700  nn0sumshdiglemB  49701