Theorem elfzelz 10260

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 10256	. 2 |- ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
2		eluzelz 9765	. 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 5326  (class class class)co 6018   ZZcz 9479   ZZ>=cuz 9755   ...cfz 10243

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-setind 4635  ax-cnex 8123  ax-resscn 8124

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-mpt 4152  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-fv 5334  df-ov 6021  df-oprab 6022  df-mpo 6023  df-neg 8353  df-z 9480  df-uz 9756  df-fz 10244

This theorem is referenced by:  elfzelzd  10261  elfz1eq  10270  fzsplit2  10285  fzdisj  10287  elfznn  10289  fznatpl1  10311  fzdifsuc  10316  fzrev2i  10321  fzrev3i  10323  elfzp12  10334  fznuz  10337  fzrevral  10340  fzshftral  10343  fznn0sub2  10363  elfzmlbm  10366  difelfznle  10370  fzosplit  10414  zsupssdc  10498  ser3mono  10749  iseqf1olemkle  10759  iseqf1olemklt  10760  iseqf1olemqcl  10761  iseqf1olemnab  10763  iseqf1olemab  10764  iseqf1olemmo  10767  iseqf1olemqk  10769  seq3f1olemqsumkj  10773  seq3f1olemqsumk  10774  seq3f1olemqsum  10775  seq3f1olemstep  10776  seqf1oglem1  10781  seqf1oglem2  10782  seqfeq4g  10793  bcval2  11012  bcval4  11014  bccmpl  11016  bcp1nk  11024  bcpasc  11028  bccl2  11030  zfz1isolemiso  11103  seq3coll  11106  swrdval2  11232  swrdlen  11233  swrdfv  11234  swrdf  11236  swrdwrdsymbg  11245  ccatswrd  11251  pfxlen  11266  ccatpfx  11282  swrdswrd  11286  pfxswrd  11287  swrdpfx  11288  lenrevpfxcctswrd  11293  pfxccatin12lem2a  11308  pfxccatin12lem1  11309  swrdccatin2  11310  pfxccatin12lem2  11312  pfxccatin12  11314  pfxccat3  11315  swrdccat3blem  11320  seq3shft  11399  sumrbdclem  11939  summodclem2a  11943  fsum0diaglem  12002  fisum0diag  12003  mptfzshft  12004  fsumrev  12005  fsumshft  12006  fsumshftm  12007  fisum0diag2  12009  binomlem  12045  binom11  12048  bcxmas  12051  arisum  12060  geo2sum  12076  cvgratnnlemabsle  12089  cvgratnnlemrate  12092  mertenslemub  12096  mertenslemi1  12097  prodfap0  12107  prodrbdclem  12133  prodmodclem2a  12138  fprodntrivap  12146  fprodm1  12160  fprod1p  12161  fprodfac  12177  fprodeq0  12179  fprodshft  12180  fprodrev  12181  fprod0diagfz  12190  fzm1ndvds  12418  lcmval  12636  lcmcllem  12640  lcmledvds  12643  prmdc  12703  prmdvdsfz  12712  isprm5lem  12714  phivalfi  12785  hashdvds  12794  phiprmpw  12795  eulerthlemrprm  12802  eulerthlema  12803  prmdiveq  12809  prmdivdiv  12810  modprminv  12823  modprminveq  12824  modprm0  12828  pcfac  12924  4sqlemafi  12969  4sqlemffi  12970  4sqleminfi  12971  4sqexercise1  12972  4sqexercise2  12973  4sqlemsdc  12974  4sqlem11  12975  4sqlem12  12976  gsumfzfsumlemm  14603  ply1termlem  15468  ply1term  15469  plyaddlem1  15473  plymullem1  15474  plymullem  15476  plycoeid3  15483  dvply1  15491  wilthlem1  15706  dvdsppwf1o  15715  mersenne  15723  lgsval2lem  15741  lgsdilem2  15767  gausslemma2dlem1a  15789  gausslemma2dlem1  15792  gausslemma2dlem3  15794  gausslemma2dlem5a  15796  gausslemma2dlem5  15797  gausslemma2dlem6  15798  lgseisenlem1  15801  lgseisenlem2  15802  lgseisenlem3  15803  lgsquadlem1  15808  lgsquadlem2  15809  lgsquadlem3  15810  2lgslem1a1  15817  2lgslem1a  15819  2lgslem1b  15820  trilpolemlt1  16648  supfz  16678  inffz  16679  gsumgfsumlem  16686