Theorem elfzelz 9956

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 9952	. 2 |- ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
2		eluzelz 9471	. 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 2136   ` cfv 5187  (class class class)co 5841   ZZcz 9187   ZZ>=cuz 9462   ...cfz 9940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-14 2139  ax-ext 2147  ax-sep 4099  ax-pow 4152  ax-pr 4186  ax-setind 4513  ax-cnex 7840  ax-resscn 7841

This theorem depends on definitions:  df-bi 116  df-3or 969  df-3an 970  df-tru 1346  df-fal 1349  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ne 2336  df-ral 2448  df-rex 2449  df-rab 2452  df-v 2727  df-sbc 2951  df-dif 3117  df-un 3119  df-in 3121  df-ss 3128  df-pw 3560  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-opab 4043  df-mpt 4044  df-id 4270  df-xp 4609  df-rel 4610  df-cnv 4611  df-co 4612  df-dm 4613  df-rn 4614  df-res 4615  df-ima 4616  df-iota 5152  df-fun 5189  df-fn 5190  df-f 5191  df-fv 5195  df-ov 5844  df-oprab 5845  df-mpo 5846  df-neg 8068  df-z 9188  df-uz 9463  df-fz 9941

This theorem is referenced by:  elfzelzd  9957  elfz1eq  9966  fzsplit2  9981  fzdisj  9983  elfznn  9985  fznatpl1  10007  fzdifsuc  10012  fzrev2i  10017  fzrev3i  10019  elfzp12  10030  fznuz  10033  fzrevral  10036  fzshftral  10039  fznn0sub2  10059  elfzmlbm  10062  difelfznle  10066  fzosplit  10108  ser3mono  10409  iseqf1olemkle  10415  iseqf1olemklt  10416  iseqf1olemqcl  10417  iseqf1olemnab  10419  iseqf1olemab  10420  iseqf1olemmo  10423  iseqf1olemqk  10425  seq3f1olemqsumkj  10429  seq3f1olemqsumk  10430  seq3f1olemqsum  10431  seq3f1olemstep  10432  bcval2  10659  bcval4  10661  bccmpl  10663  bcp1nk  10671  bcpasc  10675  bccl2  10677  zfz1isolemiso  10748  seq3coll  10751  seq3shft  10776  sumrbdclem  11314  summodclem2a  11318  fsum0diaglem  11377  fisum0diag  11378  mptfzshft  11379  fsumrev  11380  fsumshft  11381  fsumshftm  11382  fisum0diag2  11384  binomlem  11420  binom11  11423  bcxmas  11426  arisum  11435  geo2sum  11451  cvgratnnlemabsle  11464  cvgratnnlemrate  11467  mertenslemub  11471  mertenslemi1  11472  prodfap0  11482  prodrbdclem  11508  prodmodclem2a  11513  fprodntrivap  11521  fprodm1  11535  fprod1p  11536  fprodfac  11552  fprodeq0  11554  fprodshft  11555  fprodrev  11556  fprod0diagfz  11565  fzm1ndvds  11790  zsupssdc  11883  lcmval  11991  lcmcllem  11995  lcmledvds  11998  prmdc  12058  prmdvdsfz  12067  isprm5lem  12069  phivalfi  12140  hashdvds  12149  phiprmpw  12150  eulerthlemrprm  12157  eulerthlema  12158  prmdiveq  12164  prmdivdiv  12165  modprminv  12177  modprminveq  12178  modprm0  12182  pcfac  12276  lgsval2lem  13511  lgsdilem2  13537  trilpolemlt1  13880  supfz  13907  inffz  13908