Theorem elfzelz 13523

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

Syntax hints:   → wi 4   ∈ wcel 2141  ‘cfv 6516  (class class class)co 7391  ℤcz 12562  ℤ_≥cuz 12833  ...cfz 13506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7713  ax-cnex 11123  ax-resscn 11124

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-fv 6524  df-ov 7394  df-oprab 7395  df-mpo 7396  df-1st 7965  df-2nd 7966  df-neg 11411  df-z 12563  df-uz 12834  df-fz 13507

This theorem is referenced by:  elfzelzd  13524  fzssz  13525  elfz1eq  13534  fzsplit2  13548  fzdisj  13550  elfznn  13552  ssfzunsnext  13568  fznatpl1  13577  fzrev2i  13588  fzrev3i  13590  fznuz  13608  fzrevral  13611  fzshftral  13614  fznn0sub2  13634  elfzmlbm  13637  difelfznle  13641  predfz  13652  fzosplit  13692  sermono  14041  seqf1olem1  14048  seqf1olem2  14049  bcval2  14312  bcval4  14314  bccmpl  14316  bcp1nk  14324  bcval5  14325  bcpasc  14328  bccl2  14330  seqcoll2  14472  swrdval2  14654  swrdwrdsymb  14670  ccatpfx  14708  swrdswrd  14712  swrdpfx  14714  pfxccatin12lem2a  14734  pfxccatin12lem1  14735  swrdccatin2  14736  pfxccatin12lem2  14738  pfxccatin12  14740  spllen  14761  cshwidxm  14815  cshwidxn  14816  lswcshw  14822  2cshwcshw  14832  cshwcshid  14834  cshwcsh2id  14835  swrds2m  14948  seqshft  15092  sumrblem  15729  summolem2a  15733  fsum0diaglem  15794  mptfzshft  15796  fsumshftm  15799  fsum0diag2  15801  binomlem  15850  binom11  15853  bcxmas  15856  arisum  15881  geo2sum  15894  mertenslem1  15905  prodfn0  15915  prodrblem  15950  prodmolem2a  15955  fprodntriv  15963  fprodser  15970  fprodrev  15998  fallfacval3  16033  fallfacfwd  16057  0fallfac  16058  binomfallfaclem1  16060  binomfallfaclem2  16061  binomrisefac  16063  fallfacval4  16064  bpolycl  16073  bpolysum  16074  bpolydiflem  16075  fsumkthpow  16077  bpoly4  16080  fzm1ndvds  16347  pwp1fsum  16416  prmdvdsfz  16731  isprm7  16734  prmdvdsbc  16752  hashdvds  16801  phiprmpw  16802  prmdiveq  16812  modprminv  16826  modprminveq  16827  modprm0  16832  4sqlem11  16982  vdwapun  17001  prmop1  17065  prmdvdsprmo  17069  prmdvdsprmop  17070  prmgaplem1  17076  prmgaplem2  17077  prmgaplcmlem1  17078  prmgaplcmlem2  17079  prmgapprmo  17089  cshwshashlem1  17122  cshwshashlem2  17123  dfod2  19595  gsummptshft  19967  srgbinomlem3  20265  srgbinomlem4  20266  srgbinomlem  20267  freshmansdream  21614  chpscmatgsummon  22893  cayhamlem1  22914  iscmet3  25343  mbfi1fseqlem4  25768  itgz  25831  itgcl  25834  ibl0  25837  iblss  25855  iblss2  25856  itgss  25862  itgeqa  25864  iblconst  25868  iblabsr  25880  iblmulc2  25881  itgsplit  25886  dvfsumlem3  26078  plyeq0lem  26258  aalioulem1  26384  cxpeq  26810  birthdaylem2  27005  wilthlem1  27120  wilthlem3  27122  ftalem5  27129  basellem3  27135  basellem4  27136  dvdsppwf1o  27238  dvdsflf1o  27239  musum  27243  ppiub  27256  chtublem  27263  mersenne  27279  bposlem1  27336  lgsval2lem  27359  lgsdilem2  27385  lgsqrlem2  27399  gausslemma2dlem1a  27417  gausslemma2dlem1  27418  gausslemma2dlem3  27420  gausslemma2dlem4  27421  gausslemma2dlem5a  27422  gausslemma2dlem5  27423  gausslemma2dlem6  27424  lgseisenlem1  27427  lgseisenlem2  27428  lgseisenlem3  27429  lgsquadlem1  27432  lgsquadlem2  27433  lgsquadlem3  27434  2lgslem1a1  27441  2lgslem1a  27443  2lgslem1b  27444  rpvmasumlem  27539  dchrisumlem1  27541  dchrisumlem2  27542  dchrmusum2  27546  dchrvmasumlem1  27547  dchrvmasum2lem  27548  dchrvmasum2if  27549  dchrvmasumlem3  27551  dchrvmasumiflem1  27553  dchrvmasumiflem2  27554  dchrisum0flblem1  27560  rpvmasum2  27564  dchrisum0lem1b  27567  dchrisum0lem1  27568  dchrisum0lem2a  27569  dchrisum0lem2  27570  dchrisum0lem3  27571  dchrmusumlem  27574  dchrvmasumlem  27575  logdivbnd  27608  pntpbnd1  27638  pntlemh  27651  pntlemf  27657  ostth2lem2  27686  axlowdimlem13  29112  axlowdimlem14  29113  axlowdimlem16  29115  crctcshlem4  29977  crctcshwlkn0  29978  erclwwlkeqlen  30178  clwwnisshclwwsn  30218  eleclclwwlknlem2  30220  erclwwlkneqlen  30227  fzm1ne1  32951  fzsplit3  32956  bcm1n  32958  ballotlemfc0  34751  ballotlemfcc  34752  ballotlemodife  34756  ballotlemimin  34764  ballotlemsgt1  34769  ballotlemsel1i  34771  ballotlemsf1o  34772  ballotlemsi  34773  ballotlemsima  34774  ballotlemfg  34784  ballotlemfrc  34785  ballotlemfrcn0  34788  revpfxsfxrev  35427  swrdrevpfx  35428  pfxwlk  35435  swrdwlk  35438  erdszelem8  35509  erdszelem9  35510  cvmliftlem7  35602  supfz  36040  inffz  36041  bcprod  36049  fwddifnp1  36476  poimirlem1  38081  poimirlem14  38094  poimirlem15  38095  poimirlem16  38096  poimirlem17  38097  poimirlem19  38099  poimirlem20  38100  poimirlem23  38103  poimirlem24  38104  poimirlem27  38107  poimirlem31  38111  poimirlem32  38112  mblfinlem2  38118  iblmulc2nc  38145  fdc  38205  lcmineqlem1  42607  lcmineqlem6  42612  lcmineqlem17  42623  aks4d1p1p1  42641  aks6d1c1  42694  hashscontpow  42700  aks6d1c5lem0  42713  aks6d1c5lem3  42715  aks6d1c5  42717  sticksstones6  42729  sticksstones7  42730  sticksstones10  42733  sticksstones12a  42735  sticksstones12  42736  aks6d1c6lem1  42748  bcled  42756  bcle2d  42757  aks5lem5a  42769  grpods  42772  unitscyglem2  42774  unitscyglem4  42776  sumcubes  42883  irrapxlem1  43360  irrapxlem2  43361  irrapxlem3  43362  pellexlem5  43371  acongrep  43518  acongeq  43521  jm2.22  43533  jm2.23  43534  jm2.26lem3  43539  jm2.27dlem2  43548  hashnzfz  44857  monoords  45837  fmul01lt1lem1  46121  fmul01lt1lem2  46122  sumnnodd  46167  limsupubuzlem  46247  dvnmul  46478  dvnprodlem1  46481  dvnprodlem2  46482  iblsplit  46501  iblspltprt  46508  itgspltprt  46514  stoweidlem3  46538  stoweidlem11  46546  stoweidlem20  46555  stoweidlem26  46561  stoweidlem34  46569  stoweidlem59  46594  stirlinglem10  46618  dirkertrigeqlem1  46633  dirkertrigeqlem2  46634  dirkertrigeqlem3  46635  dirkertrigeq  46636  dirkeritg  46637  fourierdlem11  46653  fourierdlem12  46654  fourierdlem15  46657  fourierdlem34  46676  fourierdlem41  46683  fourierdlem46  46687  fourierdlem48  46689  fourierdlem49  46690  fourierdlem50  46691  fourierdlem54  46695  fourierdlem63  46704  fourierdlem64  46705  fourierdlem65  46706  fourierdlem79  46720  fourierdlem102  46743  fourierdlem103  46744  fourierdlem104  46745  fourierdlem114  46755  elaa2lem  46768  etransclem4  46773  etransclem7  46776  etransclem8  46777  etransclem17  46786  etransclem18  46787  etransclem20  46789  etransclem23  46792  etransclem27  46796  etransclem31  46800  etransclem32  46801  etransclem35  46804  etransclem41  46810  etransclem46  46815  etransclem48  46817  iundjiun  46995  caratheodorylem1  47061  2elfz2melfz  47873  elfzelfzlble  47876  el1fzopredsuc  47881  iccpartiltu  47989  iccpartgt  47994  iccpartnel  48005  fargshiftfo  48009  altgsumbc  48935  altgsumbcALT  48936  nn0sumshdiglemA  49202  nn0sumshdiglemB  49203