Theorem elfzelzd 13363

Description: A member of a finite set of sequential integers is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)

Hypothesis

Ref	Expression
elfzelzd.1	⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))

Assertion

Ref	Expression
elfzelzd	⊢ (𝜑 → 𝐾 ∈ ℤ)

Proof of Theorem elfzelzd

Step	Hyp	Ref	Expression
1		elfzelzd.1	. 2 ⊢ (𝜑 → 𝐾 ∈ (𝑀...𝑁))
2		elfzelz 13362	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐾 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7342  ℤcz 12425  ...cfz 13345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5248  ax-nul 5255  ax-pr 5377  ax-un 7655  ax-cnex 11033  ax-resscn 11034

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-sbc 3732  df-csb 3848  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4275  df-if 4479  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5181  df-id 5523  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6436  df-fun 6486  df-fn 6487  df-f 6488  df-fv 6492  df-ov 7345  df-oprab 7346  df-mpo 7347  df-1st 7904  df-2nd 7905  df-neg 11314  df-z 12426  df-uz 12689  df-fz 13346

This theorem is referenced by:  seqf1olem1  13868  seqz  13877  seqcoll  14283  seqcoll2  14284  ccatswrd  14480  splfv1  14567  summolem2a  15527  fsumrev  15591  prodmolem2a  15744  fprod1p  15778  prmdivdiv  16586  4sqlem12  16755  efgredleme  19445  efgredlemc  19447  efgredlemb  19448  wilthlem2  26324  lgsqrlem4  26603  lgsquadlem2  26635  pntlemj  26857  fzone1  31406  swrdrn2  31511  swrdrn3  31512  swrdf1  31513  cycpmco2lem7  31684  submateqlem2  32054  ballotlemimin  32770  ballotlemsgt1  32775  ballotlemsdom  32776  ballotlemsel1i  32777  ballotlemfrceq  32793  ballotlemfrcn0  32794  ballotlemirc  32796  ballotlem1ri  32799  fsum2dsub  32885  breprexplemc  32910  circlemeth  32918  erdszelem8  33457  poimirlem2  35933  poimirlem7  35938  poimirlem24  35955  poimirlem28  35959  fzsplitnd  40294  aks4d1p7d1  40393  aks4d1p7  40394  metakunt1  40431  metakunt3  40433  metakunt4  40434  metakunt7  40437  metakunt12  40442  metakunt21  40451  metakunt22  40452  metakunt27  40457  metakunt28  40458  metakunt29  40459  metakunt32  40462  irrapxlem3  40957  fzmaxdif  41115  acongeq  41117  jm2.26  41136  monoords  43221  sumnnodd  43557  dvnprodlem1  43873  stoweidlem11  43938  stoweidlem26  43953  fourierdlem79  44112  elaa2lem  44160  etransclem1  44162  etransclem3  44164  etransclem7  44168  etransclem10  44171  etransclem15  44176  etransclem21  44182  etransclem22  44183  etransclem24  44185  etransclem25  44186  etransclem32  44193  etransclem35  44196  etransclem37  44198  etransclem38  44199  iccpartgtprec  45288