Theorem elfzelz 13584

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6573  (class class class)co 7448  ℤcz 12639  ℤ_≥cuz 12903  ...cfz 13567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-neg 11523  df-z 12640  df-uz 12904  df-fz 13568

This theorem is referenced by:  elfzelzd  13585  fzssz  13586  elfz1eq  13595  fzsplit2  13609  fzdisj  13611  elfznn  13613  ssfzunsnext  13629  fznatpl1  13638  fzrev2i  13649  fzrev3i  13651  fznuz  13666  fzrevral  13669  fzshftral  13672  fznn0sub2  13692  elfzmlbm  13695  difelfznle  13699  predfz  13710  fzosplit  13749  sermono  14085  seqf1olem1  14092  seqf1olem2  14093  bcval2  14354  bcval4  14356  bccmpl  14358  bcp1nk  14366  bcval5  14367  bcpasc  14370  bccl2  14372  seqcoll2  14514  swrdval2  14694  swrdwrdsymb  14710  addlenrevpfx  14738  ccatpfx  14749  swrdswrd  14753  swrdpfx  14755  pfxccatin12lem2a  14775  pfxccatin12lem1  14776  swrdccatin2  14777  pfxccatin12lem2  14779  pfxccatin12  14781  spllen  14802  cshwidxm  14856  cshwidxn  14857  lswcshw  14863  2cshwcshw  14874  cshwcshid  14876  cshwcsh2id  14877  swrds2m  14990  seqshft  15134  sumrblem  15759  summolem2a  15763  fsum0diaglem  15824  mptfzshft  15826  fsumshftm  15829  fsum0diag2  15831  binomlem  15877  binom11  15880  bcxmas  15883  arisum  15908  geo2sum  15921  mertenslem1  15932  prodfn0  15942  prodrblem  15977  prodmolem2a  15982  fprodntriv  15990  fprodser  15997  fprodrev  16025  fallfacval3  16060  fallfacfwd  16084  0fallfac  16085  binomfallfaclem1  16087  binomfallfaclem2  16088  binomrisefac  16090  fallfacval4  16091  bpolycl  16100  bpolysum  16101  bpolydiflem  16102  fsumkthpow  16104  bpoly4  16107  fzm1ndvds  16370  pwp1fsum  16439  prmdvdsfz  16752  isprm7  16755  prmdvdsbc  16773  hashdvds  16822  phiprmpw  16823  prmdiveq  16833  modprminv  16846  modprminveq  16847  modprm0  16852  4sqlem11  17002  vdwapun  17021  prmop1  17085  prmdvdsprmo  17089  prmdvdsprmop  17090  prmgaplem1  17096  prmgaplem2  17097  prmgaplcmlem1  17098  prmgaplcmlem2  17099  prmgapprmo  17109  cshwshashlem1  17143  cshwshashlem2  17144  dfod2  19606  gsummptshft  19978  srgbinomlem3  20255  srgbinomlem4  20256  srgbinomlem  20257  freshmansdream  21616  chpscmatgsummon  22872  cayhamlem1  22893  iscmet3  25346  mbfi1fseqlem4  25773  itgz  25836  itgcl  25839  ibl0  25842  iblss  25860  iblss2  25861  itgss  25867  itgeqa  25869  iblconst  25873  iblabsr  25885  iblmulc2  25886  itgsplit  25891  dvfsumlem3  26089  plyeq0lem  26269  aalioulem1  26392  cxpeq  26818  birthdaylem2  27013  wilthlem1  27129  wilthlem3  27131  ftalem5  27138  basellem3  27144  basellem4  27145  dvdsppwf1o  27247  dvdsflf1o  27248  musum  27252  ppiub  27266  chtublem  27273  mersenne  27289  bposlem1  27346  lgsval2lem  27369  lgsdilem2  27395  lgsqrlem2  27409  gausslemma2dlem1a  27427  gausslemma2dlem1  27428  gausslemma2dlem3  27430  gausslemma2dlem4  27431  gausslemma2dlem5a  27432  gausslemma2dlem5  27433  gausslemma2dlem6  27434  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  2lgslem1a1  27451  2lgslem1a  27453  2lgslem1b  27454  rpvmasumlem  27549  dchrisumlem1  27551  dchrisumlem2  27552  dchrmusum2  27556  dchrvmasumlem1  27557  dchrvmasum2lem  27558  dchrvmasum2if  27559  dchrvmasumlem3  27561  dchrvmasumiflem1  27563  dchrvmasumiflem2  27564  dchrisum0flblem1  27570  rpvmasum2  27574  dchrisum0lem1b  27577  dchrisum0lem1  27578  dchrisum0lem2a  27579  dchrisum0lem2  27580  dchrisum0lem3  27581  dchrmusumlem  27584  dchrvmasumlem  27585  logdivbnd  27618  pntpbnd1  27648  pntlemh  27661  pntlemf  27667  ostth2lem2  27696  axlowdimlem13  28987  axlowdimlem14  28988  axlowdimlem16  28990  crctcshlem4  29853  crctcshwlkn0  29854  erclwwlkeqlen  30051  clwwnisshclwwsn  30091  eleclclwwlknlem2  30093  erclwwlkneqlen  30100  fzm1ne1  32794  fzsplit3  32799  bcm1n  32800  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemodife  34462  ballotlemimin  34470  ballotlemsgt1  34475  ballotlemsel1i  34477  ballotlemsf1o  34478  ballotlemsi  34479  ballotlemsima  34480  ballotlemfg  34490  ballotlemfrc  34491  ballotlemfrcn0  34494  revpfxsfxrev  35083  swrdrevpfx  35084  pfxwlk  35091  swrdwlk  35094  erdszelem8  35166  erdszelem9  35167  cvmliftlem7  35259  supfz  35691  inffz  35692  bcprod  35700  fwddifnp1  36129  poimirlem1  37581  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem23  37603  poimirlem24  37604  poimirlem27  37607  poimirlem31  37611  poimirlem32  37612  mblfinlem2  37618  iblmulc2nc  37645  fdc  37705  lcmineqlem1  41986  lcmineqlem6  41991  lcmineqlem17  42002  aks4d1p1p1  42020  aks6d1c1  42073  hashscontpow  42079  aks6d1c5lem0  42092  aks6d1c5lem3  42094  aks6d1c5  42096  sticksstones6  42108  sticksstones7  42109  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  aks6d1c6lem1  42127  bcled  42135  bcle2d  42136  aks5lem5a  42148  grpods  42151  unitscyglem2  42153  unitscyglem4  42155  metakunt15  42176  metakunt16  42177  metakunt19  42180  metakunt25  42186  metakunt33  42194  sumcubes  42301  irrapxlem1  42778  irrapxlem2  42779  irrapxlem3  42780  pellexlem5  42789  acongrep  42937  acongeq  42940  jm2.22  42952  jm2.23  42953  jm2.26lem3  42958  jm2.27dlem2  42967  hashnzfz  44289  monoords  45212  fmul01lt1lem1  45505  fmul01lt1lem2  45506  sumnnodd  45551  limsupubuzlem  45633  dvnmul  45864  dvnprodlem2  45868  iblsplit  45887  iblspltprt  45894  itgspltprt  45900  stoweidlem3  45924  stoweidlem11  45932  stoweidlem20  45941  stoweidlem26  45947  stoweidlem34  45955  stoweidlem59  45980  stirlinglem10  46004  dirkertrigeqlem1  46019  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkeritg  46023  fourierdlem11  46039  fourierdlem12  46040  fourierdlem15  46043  fourierdlem34  46062  fourierdlem41  46069  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem54  46081  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem79  46106  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem114  46141  elaa2lem  46154  etransclem4  46159  etransclem7  46162  etransclem8  46163  etransclem17  46172  etransclem18  46173  etransclem20  46175  etransclem23  46178  etransclem27  46182  etransclem31  46186  etransclem32  46187  etransclem35  46190  etransclem41  46196  etransclem46  46201  etransclem48  46203  iundjiun  46381  caratheodorylem1  46447  2elfz2melfz  47233  elfzelfzlble  47236  el1fzopredsuc  47240  iccpartiltu  47296  iccpartgt  47301  iccpartnel  47312  fargshiftfo  47316  altgsumbc  48077  altgsumbcALT  48078  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354