Theorem elfzelz 10129

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 10125	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		eluzelz 9639	. 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ ℤ)
3	1, 2	syl 14	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2175  ‘cfv 5268  (class class class)co 5934  ℤcz 9354  ℤ_≥cuz 9630  ...cfz 10112

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-setind 4583  ax-cnex 7998  ax-resscn 7999

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-ral 2488  df-rex 2489  df-rab 2492  df-v 2773  df-sbc 2998  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-opab 4105  df-mpt 4106  df-id 4338  df-xp 4679  df-rel 4680  df-cnv 4681  df-co 4682  df-dm 4683  df-rn 4684  df-res 4685  df-ima 4686  df-iota 5229  df-fun 5270  df-fn 5271  df-f 5272  df-fv 5276  df-ov 5937  df-oprab 5938  df-mpo 5939  df-neg 8228  df-z 9355  df-uz 9631  df-fz 10113

This theorem is referenced by:  elfzelzd  10130  elfz1eq  10139  fzsplit2  10154  fzdisj  10156  elfznn  10158  fznatpl1  10180  fzdifsuc  10185  fzrev2i  10190  fzrev3i  10192  elfzp12  10203  fznuz  10206  fzrevral  10209  fzshftral  10212  fznn0sub2  10232  elfzmlbm  10235  difelfznle  10239  fzosplit  10282  zsupssdc  10362  ser3mono  10613  iseqf1olemkle  10623  iseqf1olemklt  10624  iseqf1olemqcl  10625  iseqf1olemnab  10627  iseqf1olemab  10628  iseqf1olemmo  10631  iseqf1olemqk  10633  seq3f1olemqsumkj  10637  seq3f1olemqsumk  10638  seq3f1olemqsum  10639  seq3f1olemstep  10640  seqf1oglem1  10645  seqf1oglem2  10646  seqfeq4g  10657  bcval2  10876  bcval4  10878  bccmpl  10880  bcp1nk  10888  bcpasc  10892  bccl2  10894  zfz1isolemiso  10965  seq3coll  10968  seq3shft  11068  sumrbdclem  11607  summodclem2a  11611  fsum0diaglem  11670  fisum0diag  11671  mptfzshft  11672  fsumrev  11673  fsumshft  11674  fsumshftm  11675  fisum0diag2  11677  binomlem  11713  binom11  11716  bcxmas  11719  arisum  11728  geo2sum  11744  cvgratnnlemabsle  11757  cvgratnnlemrate  11760  mertenslemub  11764  mertenslemi1  11765  prodfap0  11775  prodrbdclem  11801  prodmodclem2a  11806  fprodntrivap  11814  fprodm1  11828  fprod1p  11829  fprodfac  11845  fprodeq0  11847  fprodshft  11848  fprodrev  11849  fprod0diagfz  11858  fzm1ndvds  12086  lcmval  12304  lcmcllem  12308  lcmledvds  12311  prmdc  12371  prmdvdsfz  12380  isprm5lem  12382  phivalfi  12453  hashdvds  12462  phiprmpw  12463  eulerthlemrprm  12470  eulerthlema  12471  prmdiveq  12477  prmdivdiv  12478  modprminv  12491  modprminveq  12492  modprm0  12496  pcfac  12592  4sqlemafi  12637  4sqlemffi  12638  4sqleminfi  12639  4sqexercise1  12640  4sqexercise2  12641  4sqlemsdc  12642  4sqlem11  12643  4sqlem12  12644  gsumfzfsumlemm  14267  ply1termlem  15132  ply1term  15133  plyaddlem1  15137  plymullem1  15138  plymullem  15140  plycoeid3  15147  dvply1  15155  wilthlem1  15370  dvdsppwf1o  15379  mersenne  15387  lgsval2lem  15405  lgsdilem2  15431  gausslemma2dlem1a  15453  gausslemma2dlem1  15456  gausslemma2dlem3  15458  gausslemma2dlem5a  15460  gausslemma2dlem5  15461  gausslemma2dlem6  15462  lgseisenlem1  15465  lgseisenlem2  15466  lgseisenlem3  15467  lgsquadlem1  15472  lgsquadlem2  15473  lgsquadlem3  15474  2lgslem1a1  15481  2lgslem1a  15483  2lgslem1b  15484  trilpolemlt1  15844  supfz  15874  inffz  15875