Theorem elfzelz 13548

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

Syntax hints:   → wi 4   ∈ wcel 2149  ‘cfv 6534  (class class class)co 7408  ℤcz 12587  ℤ_≥cuz 12858  ...cfz 13531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402  ax-un 7730  ax-cnex 11152  ax-resscn 11153

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-fv 6542  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7982  df-2nd 7983  df-neg 11440  df-z 12588  df-uz 12859  df-fz 13532

This theorem is referenced by:  elfzelzd  13549  fzssz  13550  elfz1eq  13559  fzsplit2  13573  fzdisj  13575  elfznn  13577  ssfzunsnext  13593  fznatpl1  13602  fzrev2i  13613  fzrev3i  13615  fznuz  13633  fzrevral  13636  fzshftral  13639  fznn0sub2  13659  elfzmlbm  13662  difelfznle  13666  predfz  13677  fzosplit  13717  sermono  14066  seqf1olem1  14073  seqf1olem2  14074  bcval2  14337  bcval4  14339  bccmpl  14341  bcp1nk  14349  bcval5  14350  bcpasc  14353  bccl2  14355  seqcoll2  14498  swrdval2  14680  swrdwrdsymb  14696  ccatpfx  14734  swrdswrd  14738  swrdpfx  14740  pfxccatin12lem2a  14760  pfxccatin12lem1  14761  swrdccatin2  14762  pfxccatin12lem2  14764  pfxccatin12  14766  spllen  14787  cshwidxm  14841  cshwidxn  14842  lswcshw  14848  2cshwcshw  14858  cshwcshid  14860  cshwcsh2id  14861  swrds2m  14974  seqshft  15118  sumrblem  15758  summolem2a  15762  fsum0diaglem  15823  mptfzshft  15825  fsumshftm  15828  fsum0diag2  15830  binomlem  15879  binom11  15882  bcxmas  15885  arisum  15910  geo2sum  15923  mertenslem1  15934  prodfn0  15944  prodrblem  15979  prodmolem2a  15984  fprodntriv  15992  fprodser  15999  fprodrev  16027  fallfacval3  16062  fallfacfwd  16086  0fallfac  16087  binomfallfaclem1  16089  binomfallfaclem2  16090  binomrisefac  16092  fallfacval4  16093  bpolycl  16102  bpolysum  16103  bpolydiflem  16104  fsumkthpow  16106  bpoly4  16109  fzm1ndvds  16376  pwp1fsum  16445  prmdvdsfz  16760  isprm7  16763  prmdvdsbc  16781  hashdvds  16830  phiprmpw  16831  prmdiveq  16841  modprminv  16855  modprminveq  16856  modprm0  16861  4sqlem11  17011  vdwapun  17030  prmop1  17094  prmdvdsprmo  17098  prmdvdsprmop  17099  prmgaplem1  17105  prmgaplem2  17106  prmgaplcmlem1  17107  prmgaplcmlem2  17108  prmgapprmo  17118  cshwshashlem1  17151  cshwshashlem2  17152  dfod2  19630  gsummptshft  20002  srgbinomlem3  20306  srgbinomlem4  20307  srgbinomlem  20308  freshmansdream  21689  chpscmatgsummon  22967  cayhamlem1  22988  iscmet3  25417  mbfi1fseqlem4  25842  itgz  25905  itgcl  25908  ibl0  25911  iblss  25929  iblss2  25930  itgss  25936  itgeqa  25938  iblconst  25942  iblabsr  25954  iblmulc2  25955  itgsplit  25960  dvfsumlem3  26152  plyeq0lem  26332  aalioulem1  26458  cxpeq  26884  birthdaylem2  27079  wilthlem1  27194  wilthlem3  27196  ftalem5  27203  basellem3  27209  basellem4  27210  dvdsppwf1o  27312  dvdsflf1o  27313  musum  27317  ppiub  27330  chtublem  27337  mersenne  27353  bposlem1  27410  lgsval2lem  27433  lgsdilem2  27459  lgsqrlem2  27473  gausslemma2dlem1a  27491  gausslemma2dlem1  27492  gausslemma2dlem3  27494  gausslemma2dlem4  27495  gausslemma2dlem5a  27496  gausslemma2dlem5  27497  gausslemma2dlem6  27498  lgseisenlem1  27501  lgseisenlem2  27502  lgseisenlem3  27503  lgsquadlem1  27506  lgsquadlem2  27507  lgsquadlem3  27508  2lgslem1a1  27515  2lgslem1a  27517  2lgslem1b  27518  rpvmasumlem  27613  dchrisumlem1  27615  dchrisumlem2  27616  dchrmusum2  27620  dchrvmasumlem1  27621  dchrvmasum2lem  27622  dchrvmasum2if  27623  dchrvmasumlem3  27625  dchrvmasumiflem1  27627  dchrvmasumiflem2  27628  dchrisum0flblem1  27634  rpvmasum2  27638  dchrisum0lem1b  27641  dchrisum0lem1  27642  dchrisum0lem2a  27643  dchrisum0lem2  27644  dchrisum0lem3  27645  dchrmusumlem  27648  dchrvmasumlem  27649  logdivbnd  27682  pntpbnd1  27712  pntlemh  27725  pntlemf  27731  ostth2lem2  27760  axlowdimlem13  29241  axlowdimlem14  29242  axlowdimlem16  29244  crctcshlem4  30106  crctcshwlkn0  30107  erclwwlkeqlen  30307  clwwnisshclwwsn  30347  eleclclwwlknlem2  30349  erclwwlkneqlen  30356  fzm1ne1  33070  fzsplit3  33075  bcm1n  33077  ballotlemfc0  34824  ballotlemfcc  34825  ballotlemodife  34829  ballotlemimin  34837  ballotlemsgt1  34842  ballotlemsel1i  34844  ballotlemsf1o  34845  ballotlemsi  34846  ballotlemsima  34847  ballotlemfg  34857  ballotlemfrc  34858  ballotlemfrcn0  34861  revpfxsfxrev  35502  swrdrevpfx  35503  pfxwlk  35511  swrdwlk  35514  erdszelem8  35585  erdszelem9  35586  cvmliftlem7  35678  supfz  36116  inffz  36117  bcprod  36125  fwddifnp1  36552  poimirlem1  38155  poimirlem14  38168  poimirlem15  38169  poimirlem16  38170  poimirlem17  38171  poimirlem19  38173  poimirlem20  38174  poimirlem23  38177  poimirlem24  38178  poimirlem27  38181  poimirlem31  38185  poimirlem32  38186  mblfinlem2  38192  iblmulc2nc  38219  fdc  38279  lcmineqlem1  42681  lcmineqlem6  42686  lcmineqlem17  42697  aks4d1p1p1  42715  aks6d1c1  42768  hashscontpow  42774  aks6d1c5lem0  42787  aks6d1c5lem3  42789  aks6d1c5  42791  sticksstones6  42803  sticksstones7  42804  sticksstones10  42807  sticksstones12a  42809  sticksstones12  42810  aks6d1c6lem1  42822  bcled  42830  bcle2d  42831  aks5lem5a  42843  grpods  42846  unitscyglem2  42848  unitscyglem4  42850  sumcubes  42959  irrapxlem1  43436  irrapxlem2  43437  irrapxlem3  43438  pellexlem5  43447  acongrep  43594  acongeq  43597  jm2.22  43609  jm2.23  43610  jm2.26lem3  43615  jm2.27dlem2  43624  hashnzfz  44917  monoords  45903  fmul01lt1lem1  46187  fmul01lt1lem2  46188  sumnnodd  46233  limsupubuzlem  46313  dvnmul  46544  dvnprodlem1  46547  dvnprodlem2  46548  iblsplit  46567  iblspltprt  46574  itgspltprt  46580  stoweidlem3  46604  stoweidlem11  46612  stoweidlem20  46621  stoweidlem26  46627  stoweidlem34  46635  stoweidlem59  46660  stirlinglem10  46684  dirkertrigeqlem1  46699  dirkertrigeqlem2  46700  dirkertrigeqlem3  46701  dirkertrigeq  46702  dirkeritg  46703  fourierdlem11  46719  fourierdlem12  46720  fourierdlem15  46723  fourierdlem34  46742  fourierdlem41  46749  fourierdlem46  46753  fourierdlem48  46755  fourierdlem49  46756  fourierdlem50  46757  fourierdlem54  46761  fourierdlem63  46770  fourierdlem64  46771  fourierdlem65  46772  fourierdlem79  46786  fourierdlem102  46809  fourierdlem103  46810  fourierdlem104  46811  fourierdlem114  46821  elaa2lem  46834  etransclem4  46839  etransclem7  46842  etransclem8  46843  etransclem17  46852  etransclem18  46853  etransclem20  46855  etransclem23  46858  etransclem27  46862  etransclem31  46866  etransclem32  46867  etransclem35  46870  etransclem41  46876  etransclem46  46881  etransclem48  46883  iundjiun  47061  caratheodorylem1  47127  2elfz2melfz  47939  elfzelfzlble  47942  el1fzopredsuc  47947  iccpartiltu  48055  iccpartgt  48060  iccpartnel  48071  fargshiftfo  48075  altgsumbc  49012  altgsumbcALT  49013  nn0sumshdiglemA  49279  nn0sumshdiglemB  49280