Theorem elfzelz 10259

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	⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

Proof of Theorem elfzelz

Step	Hyp	Ref	Expression
1		elfzuz 10255	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		eluzelz 9764	. 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ ℤ)
3	1, 2	syl 14	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2202  ‘cfv 5326  (class class class)co 6017  ℤcz 9478  ℤ_≥cuz 9754  ...cfz 10242

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 8122  ax-resscn 8123

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 6020  df-oprab 6021  df-mpo 6022  df-neg 8352  df-z 9479  df-uz 9755  df-fz 10243

This theorem is referenced by:  elfzelzd  10260  elfz1eq  10269  fzsplit2  10284  fzdisj  10286  elfznn  10288  fznatpl1  10310  fzdifsuc  10315  fzrev2i  10320  fzrev3i  10322  elfzp12  10333  fznuz  10336  fzrevral  10339  fzshftral  10342  fznn0sub2  10362  elfzmlbm  10365  difelfznle  10369  fzosplit  10413  zsupssdc  10497  ser3mono  10748  iseqf1olemkle  10758  iseqf1olemklt  10759  iseqf1olemqcl  10760  iseqf1olemnab  10762  iseqf1olemab  10763  iseqf1olemmo  10766  iseqf1olemqk  10768  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  seq3f1olemstep  10775  seqf1oglem1  10780  seqf1oglem2  10781  seqfeq4g  10792  bcval2  11011  bcval4  11013  bccmpl  11015  bcp1nk  11023  bcpasc  11027  bccl2  11029  zfz1isolemiso  11102  seq3coll  11105  swrdval2  11231  swrdlen  11232  swrdfv  11233  swrdf  11235  swrdwrdsymbg  11244  ccatswrd  11250  pfxlen  11265  ccatpfx  11281  swrdswrd  11285  pfxswrd  11286  swrdpfx  11287  lenrevpfxcctswrd  11292  pfxccatin12lem2a  11307  pfxccatin12lem1  11308  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12  11313  pfxccat3  11314  swrdccat3blem  11319  seq3shft  11398  sumrbdclem  11937  summodclem2a  11941  fsum0diaglem  12000  fisum0diag  12001  mptfzshft  12002  fsumrev  12003  fsumshft  12004  fsumshftm  12005  fisum0diag2  12007  binomlem  12043  binom11  12046  bcxmas  12049  arisum  12058  geo2sum  12074  cvgratnnlemabsle  12087  cvgratnnlemrate  12090  mertenslemub  12094  mertenslemi1  12095  prodfap0  12105  prodrbdclem  12131  prodmodclem2a  12136  fprodntrivap  12144  fprodm1  12158  fprod1p  12159  fprodfac  12175  fprodeq0  12177  fprodshft  12178  fprodrev  12179  fprod0diagfz  12188  fzm1ndvds  12416  lcmval  12634  lcmcllem  12638  lcmledvds  12641  prmdc  12701  prmdvdsfz  12710  isprm5lem  12712  phivalfi  12783  hashdvds  12792  phiprmpw  12793  eulerthlemrprm  12800  eulerthlema  12801  prmdiveq  12807  prmdivdiv  12808  modprminv  12821  modprminveq  12822  modprm0  12826  pcfac  12922  4sqlemafi  12967  4sqlemffi  12968  4sqleminfi  12969  4sqexercise1  12970  4sqexercise2  12971  4sqlemsdc  12972  4sqlem11  12973  4sqlem12  12974  gsumfzfsumlemm  14600  ply1termlem  15465  ply1term  15466  plyaddlem1  15470  plymullem1  15471  plymullem  15473  plycoeid3  15480  dvply1  15488  wilthlem1  15703  dvdsppwf1o  15712  mersenne  15720  lgsval2lem  15738  lgsdilem2  15764  gausslemma2dlem1a  15786  gausslemma2dlem1  15789  gausslemma2dlem3  15791  gausslemma2dlem5a  15793  gausslemma2dlem5  15794  gausslemma2dlem6  15795  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  2lgslem1a1  15814  2lgslem1a  15816  2lgslem1b  15817  trilpolemlt1  16645  supfz  16675  inffz  16676  gsumgfsumlem  16683