Theorem elfzelz 13492

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6514  (class class class)co 7390  ℤcz 12536  ℤ_≥cuz 12800  ...cfz 13475

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-1st 7971  df-2nd 7972  df-neg 11415  df-z 12537  df-uz 12801  df-fz 13476

This theorem is referenced by:  elfzelzd  13493  fzssz  13494  elfz1eq  13503  fzsplit2  13517  fzdisj  13519  elfznn  13521  ssfzunsnext  13537  fznatpl1  13546  fzrev2i  13557  fzrev3i  13559  fznuz  13577  fzrevral  13580  fzshftral  13583  fznn0sub2  13603  elfzmlbm  13606  difelfznle  13610  predfz  13621  fzosplit  13660  sermono  14006  seqf1olem1  14013  seqf1olem2  14014  bcval2  14277  bcval4  14279  bccmpl  14281  bcp1nk  14289  bcval5  14290  bcpasc  14293  bccl2  14295  seqcoll2  14437  swrdval2  14618  swrdwrdsymb  14634  addlenrevpfx  14662  ccatpfx  14673  swrdswrd  14677  swrdpfx  14679  pfxccatin12lem2a  14699  pfxccatin12lem1  14700  swrdccatin2  14701  pfxccatin12lem2  14703  pfxccatin12  14705  spllen  14726  cshwidxm  14780  cshwidxn  14781  lswcshw  14787  2cshwcshw  14798  cshwcshid  14800  cshwcsh2id  14801  swrds2m  14914  seqshft  15058  sumrblem  15684  summolem2a  15688  fsum0diaglem  15749  mptfzshft  15751  fsumshftm  15754  fsum0diag2  15756  binomlem  15802  binom11  15805  bcxmas  15808  arisum  15833  geo2sum  15846  mertenslem1  15857  prodfn0  15867  prodrblem  15902  prodmolem2a  15907  fprodntriv  15915  fprodser  15922  fprodrev  15950  fallfacval3  15985  fallfacfwd  16009  0fallfac  16010  binomfallfaclem1  16012  binomfallfaclem2  16013  binomrisefac  16015  fallfacval4  16016  bpolycl  16025  bpolysum  16026  bpolydiflem  16027  fsumkthpow  16029  bpoly4  16032  fzm1ndvds  16299  pwp1fsum  16368  prmdvdsfz  16682  isprm7  16685  prmdvdsbc  16703  hashdvds  16752  phiprmpw  16753  prmdiveq  16763  modprminv  16777  modprminveq  16778  modprm0  16783  4sqlem11  16933  vdwapun  16952  prmop1  17016  prmdvdsprmo  17020  prmdvdsprmop  17021  prmgaplem1  17027  prmgaplem2  17028  prmgaplcmlem1  17029  prmgaplcmlem2  17030  prmgapprmo  17040  cshwshashlem1  17073  cshwshashlem2  17074  dfod2  19501  gsummptshft  19873  srgbinomlem3  20144  srgbinomlem4  20145  srgbinomlem  20146  freshmansdream  21491  chpscmatgsummon  22739  cayhamlem1  22760  iscmet3  25200  mbfi1fseqlem4  25626  itgz  25689  itgcl  25692  ibl0  25695  iblss  25713  iblss2  25714  itgss  25720  itgeqa  25722  iblconst  25726  iblabsr  25738  iblmulc2  25739  itgsplit  25744  dvfsumlem3  25942  plyeq0lem  26122  aalioulem1  26247  cxpeq  26674  birthdaylem2  26869  wilthlem1  26985  wilthlem3  26987  ftalem5  26994  basellem3  27000  basellem4  27001  dvdsppwf1o  27103  dvdsflf1o  27104  musum  27108  ppiub  27122  chtublem  27129  mersenne  27145  bposlem1  27202  lgsval2lem  27225  lgsdilem2  27251  lgsqrlem2  27265  gausslemma2dlem1a  27283  gausslemma2dlem1  27284  gausslemma2dlem3  27286  gausslemma2dlem4  27287  gausslemma2dlem5a  27288  gausslemma2dlem5  27289  gausslemma2dlem6  27290  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  2lgslem1a1  27307  2lgslem1a  27309  2lgslem1b  27310  rpvmasumlem  27405  dchrisumlem1  27407  dchrisumlem2  27408  dchrmusum2  27412  dchrvmasumlem1  27413  dchrvmasum2lem  27414  dchrvmasum2if  27415  dchrvmasumlem3  27417  dchrvmasumiflem1  27419  dchrvmasumiflem2  27420  dchrisum0flblem1  27426  rpvmasum2  27430  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2a  27435  dchrisum0lem2  27436  dchrisum0lem3  27437  dchrmusumlem  27440  dchrvmasumlem  27441  logdivbnd  27474  pntpbnd1  27504  pntlemh  27517  pntlemf  27523  ostth2lem2  27552  axlowdimlem13  28888  axlowdimlem14  28889  axlowdimlem16  28891  crctcshlem4  29757  crctcshwlkn0  29758  erclwwlkeqlen  29955  clwwnisshclwwsn  29995  eleclclwwlknlem2  29997  erclwwlkneqlen  30004  fzm1ne1  32718  fzsplit3  32723  bcm1n  32725  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemodife  34496  ballotlemimin  34504  ballotlemsgt1  34509  ballotlemsel1i  34511  ballotlemsf1o  34512  ballotlemsi  34513  ballotlemsima  34514  ballotlemfg  34524  ballotlemfrc  34525  ballotlemfrcn0  34528  revpfxsfxrev  35110  swrdrevpfx  35111  pfxwlk  35118  swrdwlk  35121  erdszelem8  35192  erdszelem9  35193  cvmliftlem7  35285  supfz  35723  inffz  35724  bcprod  35732  fwddifnp1  36160  poimirlem1  37622  poimirlem14  37635  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem23  37644  poimirlem24  37645  poimirlem27  37648  poimirlem31  37652  poimirlem32  37653  mblfinlem2  37659  iblmulc2nc  37686  fdc  37746  lcmineqlem1  42024  lcmineqlem6  42029  lcmineqlem17  42040  aks4d1p1p1  42058  aks6d1c1  42111  hashscontpow  42117  aks6d1c5lem0  42130  aks6d1c5lem3  42132  aks6d1c5  42134  sticksstones6  42146  sticksstones7  42147  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  aks6d1c6lem1  42165  bcled  42173  bcle2d  42174  aks5lem5a  42186  grpods  42189  unitscyglem2  42191  unitscyglem4  42193  sumcubes  42308  irrapxlem1  42817  irrapxlem2  42818  irrapxlem3  42819  pellexlem5  42828  acongrep  42976  acongeq  42979  jm2.22  42991  jm2.23  42992  jm2.26lem3  42997  jm2.27dlem2  43006  hashnzfz  44316  monoords  45302  fmul01lt1lem1  45589  fmul01lt1lem2  45590  sumnnodd  45635  limsupubuzlem  45717  dvnmul  45948  dvnprodlem1  45951  dvnprodlem2  45952  iblsplit  45971  iblspltprt  45978  itgspltprt  45984  stoweidlem3  46008  stoweidlem11  46016  stoweidlem20  46025  stoweidlem26  46031  stoweidlem34  46039  stoweidlem59  46064  stirlinglem10  46088  dirkertrigeqlem1  46103  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkeritg  46107  fourierdlem11  46123  fourierdlem12  46124  fourierdlem15  46127  fourierdlem34  46146  fourierdlem41  46153  fourierdlem46  46157  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem54  46165  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem79  46190  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem114  46225  elaa2lem  46238  etransclem4  46243  etransclem7  46246  etransclem8  46247  etransclem17  46256  etransclem18  46257  etransclem20  46259  etransclem23  46262  etransclem27  46266  etransclem31  46270  etransclem32  46271  etransclem35  46274  etransclem41  46280  etransclem46  46285  etransclem48  46287  iundjiun  46465  caratheodorylem1  46531  2elfz2melfz  47323  elfzelfzlble  47326  el1fzopredsuc  47330  iccpartiltu  47427  iccpartgt  47432  iccpartnel  47443  fargshiftfo  47447  altgsumbc  48344  altgsumbcALT  48345  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613