Theorem elfzelzd 13580

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 13579	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝐾 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7414  ℤcz 12616  ...cfz 13562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737  ax-cnex 11181  ax-resscn 11182

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7987  df-2nd 7988  df-neg 11469  df-z 12617  df-uz 12889  df-fz 13563

This theorem is used by:  fzone1  13841  seqf1olem1  14106  seqz  14115  seqcoll  14530  seqcoll2  14531  swrdf1  14720  swrdrn3  14723  ccatswrd  14739  splfv1  14825  summolem2a  15802  fsumrev  15866  prodmolem2a  16022  fprod1p  16056  prmdivdiv  16879  4sqlem12  17049  pfxchn  18699  efgredleme  19871  efgredlemc  19873  efgredlemb  19874  wilthlem2  27306  lgsqrlem4  27586  lgsquadlem2  27618  pntlemj  27840  swrdrn2  33397  gsummulsubdishift1  33509  cycpmco2lem7  33573  esplyindfv  34087  submateqlem2  34319  ballotlemimin  35018  ballotlemsgt1  35023  ballotlemsdom  35024  ballotlemsel1i  35025  ballotlemfrceq  35041  ballotlemfrcn0  35042  ballotlemirc  35044  ballotlem1ri  35047  fsum2dsub  35116  breprexplemc  35141  circlemeth  35149  erdszelem8  35778  poimirlem2  38372  poimirlem7  38377  poimirlem24  38394  poimirlem28  38398  fzsplitnd  42849  aks4d1p7d1  42949  aks4d1p7  42950  primrootspoweq0  42973  hashscontpow1  42988  aks6d1c5lem1  43003  aks6d1c5lem3  43004  aks6d1c5lem2  43005  unitscyglem2  43063  irrapxlem3  43666  fzmaxdif  43823  acongeq  43825  jm2.26  43844  monoords  46131  sumnnodd  46461  dvnprodlem1  46775  stoweidlem11  46840  stoweidlem26  46855  fourierdlem79  47014  elaa2lem  47062  etransclem1  47064  etransclem3  47066  etransclem7  47070  etransclem10  47073  etransclem15  47078  etransclem21  47084  etransclem22  47085  etransclem24  47087  etransclem25  47088  etransclem32  47095  etransclem35  47098  etransclem37  47100  etransclem38  47101  iccpartgtprec  48321