Theorem elfzelz 13431

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

Syntax hints:   → wi 4   ∈ wcel 2113  ‘cfv 6489  (class class class)co 7355  ℤcz 12479  ℤ_≥cuz 12742  ...cfz 13414

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 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677  ax-cnex 11073  ax-resscn 11074

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-fv 6497  df-ov 7358  df-oprab 7359  df-mpo 7360  df-1st 7930  df-2nd 7931  df-neg 11358  df-z 12480  df-uz 12743  df-fz 13415

This theorem is referenced by:  elfzelzd  13432  fzssz  13433  elfz1eq  13442  fzsplit2  13456  fzdisj  13458  elfznn  13460  ssfzunsnext  13476  fznatpl1  13485  fzrev2i  13496  fzrev3i  13498  fznuz  13516  fzrevral  13519  fzshftral  13522  fznn0sub2  13542  elfzmlbm  13545  difelfznle  13549  predfz  13560  fzosplit  13599  sermono  13948  seqf1olem1  13955  seqf1olem2  13956  bcval2  14219  bcval4  14221  bccmpl  14223  bcp1nk  14231  bcval5  14232  bcpasc  14235  bccl2  14237  seqcoll2  14379  swrdval2  14561  swrdwrdsymb  14577  ccatpfx  14615  swrdswrd  14619  swrdpfx  14621  pfxccatin12lem2a  14641  pfxccatin12lem1  14642  swrdccatin2  14643  pfxccatin12lem2  14645  pfxccatin12  14647  spllen  14668  cshwidxm  14722  cshwidxn  14723  lswcshw  14729  2cshwcshw  14739  cshwcshid  14741  cshwcsh2id  14742  swrds2m  14855  seqshft  14999  sumrblem  15625  summolem2a  15629  fsum0diaglem  15690  mptfzshft  15692  fsumshftm  15695  fsum0diag2  15697  binomlem  15743  binom11  15746  bcxmas  15749  arisum  15774  geo2sum  15787  mertenslem1  15798  prodfn0  15808  prodrblem  15843  prodmolem2a  15848  fprodntriv  15856  fprodser  15863  fprodrev  15891  fallfacval3  15926  fallfacfwd  15950  0fallfac  15951  binomfallfaclem1  15953  binomfallfaclem2  15954  binomrisefac  15956  fallfacval4  15957  bpolycl  15966  bpolysum  15967  bpolydiflem  15968  fsumkthpow  15970  bpoly4  15973  fzm1ndvds  16240  pwp1fsum  16309  prmdvdsfz  16623  isprm7  16626  prmdvdsbc  16644  hashdvds  16693  phiprmpw  16694  prmdiveq  16704  modprminv  16718  modprminveq  16719  modprm0  16724  4sqlem11  16874  vdwapun  16893  prmop1  16957  prmdvdsprmo  16961  prmdvdsprmop  16962  prmgaplem1  16968  prmgaplem2  16969  prmgaplcmlem1  16970  prmgaplcmlem2  16971  prmgapprmo  16981  cshwshashlem1  17014  cshwshashlem2  17015  dfod2  19484  gsummptshft  19856  srgbinomlem3  20154  srgbinomlem4  20155  srgbinomlem  20156  freshmansdream  21520  chpscmatgsummon  22780  cayhamlem1  22801  iscmet3  25240  mbfi1fseqlem4  25666  itgz  25729  itgcl  25732  ibl0  25735  iblss  25753  iblss2  25754  itgss  25760  itgeqa  25762  iblconst  25766  iblabsr  25778  iblmulc2  25779  itgsplit  25784  dvfsumlem3  25982  plyeq0lem  26162  aalioulem1  26287  cxpeq  26714  birthdaylem2  26909  wilthlem1  27025  wilthlem3  27027  ftalem5  27034  basellem3  27040  basellem4  27041  dvdsppwf1o  27143  dvdsflf1o  27144  musum  27148  ppiub  27162  chtublem  27169  mersenne  27185  bposlem1  27242  lgsval2lem  27265  lgsdilem2  27291  lgsqrlem2  27305  gausslemma2dlem1a  27323  gausslemma2dlem1  27324  gausslemma2dlem3  27326  gausslemma2dlem4  27327  gausslemma2dlem5a  27328  gausslemma2dlem5  27329  gausslemma2dlem6  27330  lgseisenlem1  27333  lgseisenlem2  27334  lgseisenlem3  27335  lgsquadlem1  27338  lgsquadlem2  27339  lgsquadlem3  27340  2lgslem1a1  27347  2lgslem1a  27349  2lgslem1b  27350  rpvmasumlem  27445  dchrisumlem1  27447  dchrisumlem2  27448  dchrmusum2  27452  dchrvmasumlem1  27453  dchrvmasum2lem  27454  dchrvmasum2if  27455  dchrvmasumlem3  27457  dchrvmasumiflem1  27459  dchrvmasumiflem2  27460  dchrisum0flblem1  27466  rpvmasum2  27470  dchrisum0lem1b  27473  dchrisum0lem1  27474  dchrisum0lem2a  27475  dchrisum0lem2  27476  dchrisum0lem3  27477  dchrmusumlem  27480  dchrvmasumlem  27481  logdivbnd  27514  pntpbnd1  27544  pntlemh  27557  pntlemf  27563  ostth2lem2  27592  axlowdimlem13  28953  axlowdimlem14  28954  axlowdimlem16  28956  crctcshlem4  29819  crctcshwlkn0  29820  erclwwlkeqlen  30020  clwwnisshclwwsn  30060  eleclclwwlknlem2  30062  erclwwlkneqlen  30069  fzm1ne1  32796  fzsplit3  32801  bcm1n  32803  ballotlemfc0  34578  ballotlemfcc  34579  ballotlemodife  34583  ballotlemimin  34591  ballotlemsgt1  34596  ballotlemsel1i  34598  ballotlemsf1o  34599  ballotlemsi  34600  ballotlemsima  34601  ballotlemfg  34611  ballotlemfrc  34612  ballotlemfrcn0  34615  revpfxsfxrev  35232  swrdrevpfx  35233  pfxwlk  35240  swrdwlk  35243  erdszelem8  35314  erdszelem9  35315  cvmliftlem7  35407  supfz  35845  inffz  35846  bcprod  35854  fwddifnp1  36281  poimirlem1  37734  poimirlem14  37747  poimirlem15  37748  poimirlem16  37749  poimirlem17  37750  poimirlem19  37752  poimirlem20  37753  poimirlem23  37756  poimirlem24  37757  poimirlem27  37760  poimirlem31  37764  poimirlem32  37765  mblfinlem2  37771  iblmulc2nc  37798  fdc  37858  lcmineqlem1  42195  lcmineqlem6  42200  lcmineqlem17  42211  aks4d1p1p1  42229  aks6d1c1  42282  hashscontpow  42288  aks6d1c5lem0  42301  aks6d1c5lem3  42303  aks6d1c5  42305  sticksstones6  42317  sticksstones7  42318  sticksstones10  42321  sticksstones12a  42323  sticksstones12  42324  aks6d1c6lem1  42336  bcled  42344  bcle2d  42345  aks5lem5a  42357  grpods  42360  unitscyglem2  42362  unitscyglem4  42364  sumcubes  42483  irrapxlem1  42979  irrapxlem2  42980  irrapxlem3  42981  pellexlem5  42990  acongrep  43137  acongeq  43140  jm2.22  43152  jm2.23  43153  jm2.26lem3  43158  jm2.27dlem2  43167  hashnzfz  44477  monoords  45461  fmul01lt1lem1  45746  fmul01lt1lem2  45747  sumnnodd  45792  limsupubuzlem  45872  dvnmul  46103  dvnprodlem1  46106  dvnprodlem2  46107  iblsplit  46126  iblspltprt  46133  itgspltprt  46139  stoweidlem3  46163  stoweidlem11  46171  stoweidlem20  46180  stoweidlem26  46186  stoweidlem34  46194  stoweidlem59  46219  stirlinglem10  46243  dirkertrigeqlem1  46258  dirkertrigeqlem2  46259  dirkertrigeqlem3  46260  dirkertrigeq  46261  dirkeritg  46262  fourierdlem11  46278  fourierdlem12  46279  fourierdlem15  46282  fourierdlem34  46301  fourierdlem41  46308  fourierdlem46  46312  fourierdlem48  46314  fourierdlem49  46315  fourierdlem50  46316  fourierdlem54  46320  fourierdlem63  46329  fourierdlem64  46330  fourierdlem65  46331  fourierdlem79  46345  fourierdlem102  46368  fourierdlem103  46369  fourierdlem104  46370  fourierdlem114  46380  elaa2lem  46393  etransclem4  46398  etransclem7  46401  etransclem8  46402  etransclem17  46411  etransclem18  46412  etransclem20  46414  etransclem23  46417  etransclem27  46421  etransclem31  46425  etransclem32  46426  etransclem35  46429  etransclem41  46435  etransclem46  46440  etransclem48  46442  iundjiun  46620  caratheodorylem1  46686  2elfz2melfz  47480  elfzelfzlble  47483  el1fzopredsuc  47487  iccpartiltu  47584  iccpartgt  47589  iccpartnel  47600  fargshiftfo  47604  altgsumbc  48514  altgsumbcALT  48515  nn0sumshdiglemA  48781  nn0sumshdiglemB  48782