Theorem elfzelz 10103

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 10099	. 2 |- ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
2		eluzelz 9613	. 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 2167   ` cfv 5259  (class class class)co 5923   ZZcz 9329   ZZ>=cuz 9604   ...cfz 10086

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4152  ax-pow 4208  ax-pr 4243  ax-setind 4574  ax-cnex 7973  ax-resscn 7974

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-ral 2480  df-rex 2481  df-rab 2484  df-v 2765  df-sbc 2990  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-opab 4096  df-mpt 4097  df-id 4329  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-rn 4675  df-res 4676  df-ima 4677  df-iota 5220  df-fun 5261  df-fn 5262  df-f 5263  df-fv 5267  df-ov 5926  df-oprab 5927  df-mpo 5928  df-neg 8203  df-z 9330  df-uz 9605  df-fz 10087

This theorem is referenced by:  elfzelzd  10104  elfz1eq  10113  fzsplit2  10128  fzdisj  10130  elfznn  10132  fznatpl1  10154  fzdifsuc  10159  fzrev2i  10164  fzrev3i  10166  elfzp12  10177  fznuz  10180  fzrevral  10183  fzshftral  10186  fznn0sub2  10206  elfzmlbm  10209  difelfznle  10213  fzosplit  10256  zsupssdc  10331  ser3mono  10582  iseqf1olemkle  10592  iseqf1olemklt  10593  iseqf1olemqcl  10594  iseqf1olemnab  10596  iseqf1olemab  10597  iseqf1olemmo  10600  iseqf1olemqk  10602  seq3f1olemqsumkj  10606  seq3f1olemqsumk  10607  seq3f1olemqsum  10608  seq3f1olemstep  10609  seqf1oglem1  10614  seqf1oglem2  10615  seqfeq4g  10626  bcval2  10845  bcval4  10847  bccmpl  10849  bcp1nk  10857  bcpasc  10861  bccl2  10863  zfz1isolemiso  10934  seq3coll  10937  seq3shft  11006  sumrbdclem  11545  summodclem2a  11549  fsum0diaglem  11608  fisum0diag  11609  mptfzshft  11610  fsumrev  11611  fsumshft  11612  fsumshftm  11613  fisum0diag2  11615  binomlem  11651  binom11  11654  bcxmas  11657  arisum  11666  geo2sum  11682  cvgratnnlemabsle  11695  cvgratnnlemrate  11698  mertenslemub  11702  mertenslemi1  11703  prodfap0  11713  prodrbdclem  11739  prodmodclem2a  11744  fprodntrivap  11752  fprodm1  11766  fprod1p  11767  fprodfac  11783  fprodeq0  11785  fprodshft  11786  fprodrev  11787  fprod0diagfz  11796  fzm1ndvds  12024  lcmval  12242  lcmcllem  12246  lcmledvds  12249  prmdc  12309  prmdvdsfz  12318  isprm5lem  12320  phivalfi  12391  hashdvds  12400  phiprmpw  12401  eulerthlemrprm  12408  eulerthlema  12409  prmdiveq  12415  prmdivdiv  12416  modprminv  12429  modprminveq  12430  modprm0  12434  pcfac  12530  4sqlemafi  12575  4sqlemffi  12576  4sqleminfi  12577  4sqexercise1  12578  4sqexercise2  12579  4sqlemsdc  12580  4sqlem11  12581  4sqlem12  12582  gsumfzfsumlemm  14169  ply1termlem  15004  ply1term  15005  plyaddlem1  15009  plymullem1  15010  plymullem  15012  plycoeid3  15019  dvply1  15027  wilthlem1  15242  dvdsppwf1o  15251  mersenne  15259  lgsval2lem  15277  lgsdilem2  15303  gausslemma2dlem1a  15325  gausslemma2dlem1  15328  gausslemma2dlem3  15330  gausslemma2dlem5a  15332  gausslemma2dlem5  15333  gausslemma2dlem6  15334  lgseisenlem1  15337  lgseisenlem2  15338  lgseisenlem3  15339  lgsquadlem1  15344  lgsquadlem2  15345  lgsquadlem3  15346  2lgslem1a1  15353  2lgslem1a  15355  2lgslem1b  15356  trilpolemlt1  15714  supfz  15744  inffz  15745