Theorem elfzelzd 13565

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7431  ℤcz 12613  ...cfz 13547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-neg 11495  df-z 12614  df-uz 12879  df-fz 13548

This theorem is referenced by:  seqf1olem1  14082  seqz  14091  seqcoll  14503  seqcoll2  14504  ccatswrd  14706  splfv1  14793  summolem2a  15751  fsumrev  15815  prodmolem2a  15970  fprod1p  16004  prmdivdiv  16824  4sqlem12  16994  efgredleme  19761  efgredlemc  19763  efgredlemb  19764  wilthlem2  27112  lgsqrlem4  27393  lgsquadlem2  27425  pntlemj  27647  fzone1  32802  swrdrn2  32939  swrdrn3  32940  swrdf1  32941  pfxchn  32999  cycpmco2lem7  33152  submateqlem2  33807  ballotlemimin  34508  ballotlemsgt1  34513  ballotlemsdom  34514  ballotlemsel1i  34515  ballotlemfrceq  34531  ballotlemfrcn0  34532  ballotlemirc  34534  ballotlem1ri  34537  fsum2dsub  34622  breprexplemc  34647  circlemeth  34655  erdszelem8  35203  poimirlem2  37629  poimirlem7  37634  poimirlem24  37651  poimirlem28  37655  fzsplitnd  41983  aks4d1p7d1  42083  aks4d1p7  42084  primrootspoweq0  42107  hashscontpow1  42122  aks6d1c5lem1  42137  aks6d1c5lem3  42138  aks6d1c5lem2  42139  unitscyglem2  42197  metakunt1  42206  metakunt3  42208  metakunt4  42209  metakunt7  42212  metakunt12  42217  metakunt21  42226  metakunt22  42227  metakunt27  42232  metakunt28  42233  metakunt29  42234  metakunt32  42237  irrapxlem3  42835  fzmaxdif  42993  acongeq  42995  jm2.26  43014  monoords  45309  sumnnodd  45645  dvnprodlem1  45961  stoweidlem11  46026  stoweidlem26  46041  fourierdlem79  46200  elaa2lem  46248  etransclem1  46250  etransclem3  46252  etransclem7  46256  etransclem10  46259  etransclem15  46264  etransclem21  46270  etransclem22  46271  etransclem24  46273  etransclem25  46274  etransclem32  46281  etransclem35  46284  etransclem37  46286  etransclem38  46287  iccpartgtprec  47407