Theorem elfzelz 13440

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

Syntax hints:   → wi 4   ∈ wcel 2113  ‘cfv 6492  (class class class)co 7358  ℤcz 12488  ℤ_≥cuz 12751  ...cfz 13423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934  df-neg 11367  df-z 12489  df-uz 12752  df-fz 13424

This theorem is referenced by:  elfzelzd  13441  fzssz  13442  elfz1eq  13451  fzsplit2  13465  fzdisj  13467  elfznn  13469  ssfzunsnext  13485  fznatpl1  13494  fzrev2i  13505  fzrev3i  13507  fznuz  13525  fzrevral  13528  fzshftral  13531  fznn0sub2  13551  elfzmlbm  13554  difelfznle  13558  predfz  13569  fzosplit  13608  sermono  13957  seqf1olem1  13964  seqf1olem2  13965  bcval2  14228  bcval4  14230  bccmpl  14232  bcp1nk  14240  bcval5  14241  bcpasc  14244  bccl2  14246  seqcoll2  14388  swrdval2  14570  swrdwrdsymb  14586  ccatpfx  14624  swrdswrd  14628  swrdpfx  14630  pfxccatin12lem2a  14650  pfxccatin12lem1  14651  swrdccatin2  14652  pfxccatin12lem2  14654  pfxccatin12  14656  spllen  14677  cshwidxm  14731  cshwidxn  14732  lswcshw  14738  2cshwcshw  14748  cshwcshid  14750  cshwcsh2id  14751  swrds2m  14864  seqshft  15008  sumrblem  15634  summolem2a  15638  fsum0diaglem  15699  mptfzshft  15701  fsumshftm  15704  fsum0diag2  15706  binomlem  15752  binom11  15755  bcxmas  15758  arisum  15783  geo2sum  15796  mertenslem1  15807  prodfn0  15817  prodrblem  15852  prodmolem2a  15857  fprodntriv  15865  fprodser  15872  fprodrev  15900  fallfacval3  15935  fallfacfwd  15959  0fallfac  15960  binomfallfaclem1  15962  binomfallfaclem2  15963  binomrisefac  15965  fallfacval4  15966  bpolycl  15975  bpolysum  15976  bpolydiflem  15977  fsumkthpow  15979  bpoly4  15982  fzm1ndvds  16249  pwp1fsum  16318  prmdvdsfz  16632  isprm7  16635  prmdvdsbc  16653  hashdvds  16702  phiprmpw  16703  prmdiveq  16713  modprminv  16727  modprminveq  16728  modprm0  16733  4sqlem11  16883  vdwapun  16902  prmop1  16966  prmdvdsprmo  16970  prmdvdsprmop  16971  prmgaplem1  16977  prmgaplem2  16978  prmgaplcmlem1  16979  prmgaplcmlem2  16980  prmgapprmo  16990  cshwshashlem1  17023  cshwshashlem2  17024  dfod2  19493  gsummptshft  19865  srgbinomlem3  20163  srgbinomlem4  20164  srgbinomlem  20165  freshmansdream  21529  chpscmatgsummon  22789  cayhamlem1  22810  iscmet3  25249  mbfi1fseqlem4  25675  itgz  25738  itgcl  25741  ibl0  25744  iblss  25762  iblss2  25763  itgss  25769  itgeqa  25771  iblconst  25775  iblabsr  25787  iblmulc2  25788  itgsplit  25793  dvfsumlem3  25991  plyeq0lem  26171  aalioulem1  26296  cxpeq  26723  birthdaylem2  26918  wilthlem1  27034  wilthlem3  27036  ftalem5  27043  basellem3  27049  basellem4  27050  dvdsppwf1o  27152  dvdsflf1o  27153  musum  27157  ppiub  27171  chtublem  27178  mersenne  27194  bposlem1  27251  lgsval2lem  27274  lgsdilem2  27300  lgsqrlem2  27314  gausslemma2dlem1a  27332  gausslemma2dlem1  27333  gausslemma2dlem3  27335  gausslemma2dlem4  27336  gausslemma2dlem5a  27337  gausslemma2dlem5  27338  gausslemma2dlem6  27339  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  2lgslem1a1  27356  2lgslem1a  27358  2lgslem1b  27359  rpvmasumlem  27454  dchrisumlem1  27456  dchrisumlem2  27457  dchrmusum2  27461  dchrvmasumlem1  27462  dchrvmasum2lem  27463  dchrvmasum2if  27464  dchrvmasumlem3  27466  dchrvmasumiflem1  27468  dchrvmasumiflem2  27469  dchrisum0flblem1  27475  rpvmasum2  27479  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0lem2a  27484  dchrisum0lem2  27485  dchrisum0lem3  27486  dchrmusumlem  27489  dchrvmasumlem  27490  logdivbnd  27523  pntpbnd1  27553  pntlemh  27566  pntlemf  27572  ostth2lem2  27601  axlowdimlem13  29027  axlowdimlem14  29028  axlowdimlem16  29030  crctcshlem4  29893  crctcshwlkn0  29894  erclwwlkeqlen  30094  clwwnisshclwwsn  30134  eleclclwwlknlem2  30136  erclwwlkneqlen  30143  fzm1ne1  32868  fzsplit3  32873  bcm1n  32875  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemodife  34655  ballotlemimin  34663  ballotlemsgt1  34668  ballotlemsel1i  34670  ballotlemsf1o  34671  ballotlemsi  34672  ballotlemsima  34673  ballotlemfg  34683  ballotlemfrc  34684  ballotlemfrcn0  34687  revpfxsfxrev  35310  swrdrevpfx  35311  pfxwlk  35318  swrdwlk  35321  erdszelem8  35392  erdszelem9  35393  cvmliftlem7  35485  supfz  35923  inffz  35924  bcprod  35932  fwddifnp1  36359  poimirlem1  37822  poimirlem14  37835  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem23  37844  poimirlem24  37845  poimirlem27  37848  poimirlem31  37852  poimirlem32  37853  mblfinlem2  37859  iblmulc2nc  37886  fdc  37946  lcmineqlem1  42283  lcmineqlem6  42288  lcmineqlem17  42299  aks4d1p1p1  42317  aks6d1c1  42370  hashscontpow  42376  aks6d1c5lem0  42389  aks6d1c5lem3  42391  aks6d1c5  42393  sticksstones6  42405  sticksstones7  42406  sticksstones10  42409  sticksstones12a  42411  sticksstones12  42412  aks6d1c6lem1  42424  bcled  42432  bcle2d  42433  aks5lem5a  42445  grpods  42448  unitscyglem2  42450  unitscyglem4  42452  sumcubes  42568  irrapxlem1  43064  irrapxlem2  43065  irrapxlem3  43066  pellexlem5  43075  acongrep  43222  acongeq  43225  jm2.22  43237  jm2.23  43238  jm2.26lem3  43243  jm2.27dlem2  43252  hashnzfz  44561  monoords  45545  fmul01lt1lem1  45830  fmul01lt1lem2  45831  sumnnodd  45876  limsupubuzlem  45956  dvnmul  46187  dvnprodlem1  46190  dvnprodlem2  46191  iblsplit  46210  iblspltprt  46217  itgspltprt  46223  stoweidlem3  46247  stoweidlem11  46255  stoweidlem20  46264  stoweidlem26  46270  stoweidlem34  46278  stoweidlem59  46303  stirlinglem10  46327  dirkertrigeqlem1  46342  dirkertrigeqlem2  46343  dirkertrigeqlem3  46344  dirkertrigeq  46345  dirkeritg  46346  fourierdlem11  46362  fourierdlem12  46363  fourierdlem15  46366  fourierdlem34  46385  fourierdlem41  46392  fourierdlem46  46396  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem54  46404  fourierdlem63  46413  fourierdlem64  46414  fourierdlem65  46415  fourierdlem79  46429  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem114  46464  elaa2lem  46477  etransclem4  46482  etransclem7  46485  etransclem8  46486  etransclem17  46495  etransclem18  46496  etransclem20  46498  etransclem23  46501  etransclem27  46505  etransclem31  46509  etransclem32  46510  etransclem35  46513  etransclem41  46519  etransclem46  46524  etransclem48  46526  iundjiun  46704  caratheodorylem1  46770  2elfz2melfz  47564  elfzelfzlble  47567  el1fzopredsuc  47571  iccpartiltu  47668  iccpartgt  47673  iccpartnel  47684  fargshiftfo  47688  altgsumbc  48598  altgsumbcALT  48599  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866