Theorem elfzelz 10322

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 10318	. 2 |- ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
2		eluzelz 9826	. 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 2202   ` cfv 5333  (class class class)co 6028   ZZcz 9540   ZZ>=cuz 9816   ...cfz 10305

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-setind 4641  ax-cnex 8183  ax-resscn 8184

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-ral 2516  df-rex 2517  df-rab 2520  df-v 2805  df-sbc 3033  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-mpt 4157  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-res 4743  df-ima 4744  df-iota 5293  df-fun 5335  df-fn 5336  df-f 5337  df-fv 5341  df-ov 6031  df-oprab 6032  df-mpo 6033  df-neg 8412  df-z 9541  df-uz 9817  df-fz 10306

This theorem is referenced by:  elfzelzd  10323  elfz1eq  10332  fzsplit2  10347  fzdisj  10349  elfznn  10351  fznatpl1  10373  fzdifsuc  10378  fzrev2i  10383  fzrev3i  10385  elfzp12  10396  fznuz  10399  fzrevral  10402  fzshftral  10405  fznn0sub2  10425  elfzmlbm  10428  difelfznle  10432  fzosplit  10476  zsupssdc  10561  ser3mono  10812  iseqf1olemkle  10822  iseqf1olemklt  10823  iseqf1olemqcl  10824  iseqf1olemnab  10826  iseqf1olemab  10827  iseqf1olemmo  10830  iseqf1olemqk  10832  seq3f1olemqsumkj  10836  seq3f1olemqsumk  10837  seq3f1olemqsum  10838  seq3f1olemstep  10839  seqf1oglem1  10844  seqf1oglem2  10845  seqfeq4g  10856  bcval2  11075  bcval4  11077  bccmpl  11079  bcp1nk  11087  bcpasc  11091  bccl2  11093  zfz1isolemiso  11166  seq3coll  11169  swrdval2  11298  swrdlen  11299  swrdfv  11300  swrdf  11302  swrdwrdsymbg  11311  ccatswrd  11317  pfxlen  11332  ccatpfx  11348  swrdswrd  11352  pfxswrd  11353  swrdpfx  11354  lenrevpfxcctswrd  11359  pfxccatin12lem2a  11374  pfxccatin12lem1  11375  swrdccatin2  11376  pfxccatin12lem2  11378  pfxccatin12  11380  pfxccat3  11381  swrdccat3blem  11386  seq3shft  11478  sumrbdclem  12018  summodclem2a  12022  fsum0diaglem  12081  fisum0diag  12082  mptfzshft  12083  fsumrev  12084  fsumshft  12085  fsumshftm  12086  fisum0diag2  12088  binomlem  12124  binom11  12127  bcxmas  12130  arisum  12139  geo2sum  12155  cvgratnnlemabsle  12168  cvgratnnlemrate  12171  mertenslemub  12175  mertenslemi1  12176  prodfap0  12186  prodrbdclem  12212  prodmodclem2a  12217  fprodntrivap  12225  fprodm1  12239  fprod1p  12240  fprodfac  12256  fprodeq0  12258  fprodshft  12259  fprodrev  12260  fprod0diagfz  12269  fzm1ndvds  12497  lcmval  12715  lcmcllem  12719  lcmledvds  12722  prmdc  12782  prmdvdsfz  12791  isprm5lem  12793  phivalfi  12864  hashdvds  12873  phiprmpw  12874  eulerthlemrprm  12881  eulerthlema  12882  prmdiveq  12888  prmdivdiv  12889  modprminv  12902  modprminveq  12903  modprm0  12907  pcfac  13003  4sqlemafi  13048  4sqlemffi  13049  4sqleminfi  13050  4sqexercise1  13051  4sqexercise2  13052  4sqlemsdc  13053  4sqlem11  13054  4sqlem12  13055  gsumfzfsumlemm  14683  ply1termlem  15553  ply1term  15554  plyaddlem1  15558  plymullem1  15559  plymullem  15561  plycoeid3  15568  dvply1  15576  wilthlem1  15794  dvdsppwf1o  15803  mersenne  15811  lgsval2lem  15829  lgsdilem2  15855  gausslemma2dlem1a  15877  gausslemma2dlem1  15880  gausslemma2dlem3  15882  gausslemma2dlem5a  15884  gausslemma2dlem5  15885  gausslemma2dlem6  15886  lgseisenlem1  15889  lgseisenlem2  15890  lgseisenlem3  15891  lgsquadlem1  15896  lgsquadlem2  15897  lgsquadlem3  15898  2lgslem1a1  15905  2lgslem1a  15907  2lgslem1b  15908  trilpolemlt1  16773  supfz  16804  inffz  16805  gsumgfsumlem  16812