Theorem elfzelz 10182

Description: A member of a finite set of sequential integer is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzelz	|- ( K e. ( M ... N ) -> K e. ZZ )

Proof of Theorem elfzelz

Step	Hyp	Ref	Expression
1		elfzuz 10178	. 2 |- ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
2		eluzelz 9692	. 2 |- ( K e. ( ZZ>= ` M ) -> K e. ZZ )
3	1, 2	syl 14	1 |- ( K e. ( M ... N ) -> K e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2178   ` cfv 5290  (class class class)co 5967   ZZcz 9407   ZZ>=cuz 9683   ...cfz 10165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269  ax-setind 4603  ax-cnex 8051  ax-resscn 8052

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ne 2379  df-ral 2491  df-rex 2492  df-rab 2495  df-v 2778  df-sbc 3006  df-dif 3176  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-opab 4122  df-mpt 4123  df-id 4358  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-rn 4704  df-res 4705  df-ima 4706  df-iota 5251  df-fun 5292  df-fn 5293  df-f 5294  df-fv 5298  df-ov 5970  df-oprab 5971  df-mpo 5972  df-neg 8281  df-z 9408  df-uz 9684  df-fz 10166

This theorem is referenced by:  elfzelzd  10183  elfz1eq  10192  fzsplit2  10207  fzdisj  10209  elfznn  10211  fznatpl1  10233  fzdifsuc  10238  fzrev2i  10243  fzrev3i  10245  elfzp12  10256  fznuz  10259  fzrevral  10262  fzshftral  10265  fznn0sub2  10285  elfzmlbm  10288  difelfznle  10292  fzosplit  10336  zsupssdc  10418  ser3mono  10669  iseqf1olemkle  10679  iseqf1olemklt  10680  iseqf1olemqcl  10681  iseqf1olemnab  10683  iseqf1olemab  10684  iseqf1olemmo  10687  iseqf1olemqk  10689  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seq3f1olemqsum  10695  seq3f1olemstep  10696  seqf1oglem1  10701  seqf1oglem2  10702  seqfeq4g  10713  bcval2  10932  bcval4  10934  bccmpl  10936  bcp1nk  10944  bcpasc  10948  bccl2  10950  zfz1isolemiso  11021  seq3coll  11024  swrdval2  11142  swrdlen  11143  swrdfv  11144  swrdf  11146  swrdwrdsymbg  11155  ccatswrd  11161  pfxlen  11176  ccatpfx  11192  swrdswrd  11196  pfxswrd  11197  swrdpfx  11198  lenrevpfxcctswrd  11203  pfxccatin12lem2a  11218  pfxccatin12lem1  11219  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccatin12  11224  pfxccat3  11225  swrdccat3blem  11230  seq3shft  11264  sumrbdclem  11803  summodclem2a  11807  fsum0diaglem  11866  fisum0diag  11867  mptfzshft  11868  fsumrev  11869  fsumshft  11870  fsumshftm  11871  fisum0diag2  11873  binomlem  11909  binom11  11912  bcxmas  11915  arisum  11924  geo2sum  11940  cvgratnnlemabsle  11953  cvgratnnlemrate  11956  mertenslemub  11960  mertenslemi1  11961  prodfap0  11971  prodrbdclem  11997  prodmodclem2a  12002  fprodntrivap  12010  fprodm1  12024  fprod1p  12025  fprodfac  12041  fprodeq0  12043  fprodshft  12044  fprodrev  12045  fprod0diagfz  12054  fzm1ndvds  12282  lcmval  12500  lcmcllem  12504  lcmledvds  12507  prmdc  12567  prmdvdsfz  12576  isprm5lem  12578  phivalfi  12649  hashdvds  12658  phiprmpw  12659  eulerthlemrprm  12666  eulerthlema  12667  prmdiveq  12673  prmdivdiv  12674  modprminv  12687  modprminveq  12688  modprm0  12692  pcfac  12788  4sqlemafi  12833  4sqlemffi  12834  4sqleminfi  12835  4sqexercise1  12836  4sqexercise2  12837  4sqlemsdc  12838  4sqlem11  12839  4sqlem12  12840  gsumfzfsumlemm  14464  ply1termlem  15329  ply1term  15330  plyaddlem1  15334  plymullem1  15335  plymullem  15337  plycoeid3  15344  dvply1  15352  wilthlem1  15567  dvdsppwf1o  15576  mersenne  15584  lgsval2lem  15602  lgsdilem2  15628  gausslemma2dlem1a  15650  gausslemma2dlem1  15653  gausslemma2dlem3  15655  gausslemma2dlem5a  15657  gausslemma2dlem5  15658  gausslemma2dlem6  15659  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  2lgslem1a1  15678  2lgslem1a  15680  2lgslem1b  15681  trilpolemlt1  16182  supfz  16212  inffz  16213