Theorem elfzelzd 13473

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7361  ℤcz 12518  ...cfz 13455

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  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 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7936  df-2nd 7937  df-neg 11374  df-z 12519  df-uz 12783  df-fz 13456

This theorem is referenced by:  fzone1  13733  seqf1olem1  13997  seqz  14006  seqcoll  14420  seqcoll2  14421  ccatswrd  14625  splfv1  14711  summolem2a  15671  fsumrev  15735  prodmolem2a  15893  fprod1p  15927  prmdivdiv  16751  4sqlem12  16921  pfxchn  18570  efgredleme  19712  efgredlemc  19714  efgredlemb  19715  wilthlem2  27049  lgsqrlem4  27329  lgsquadlem2  27361  pntlemj  27583  swrdrn2  33032  swrdrn3  33033  swrdf1  33034  gsummulsubdishift1  33147  cycpmco2lem7  33211  esplyindfv  33738  submateqlem2  33971  ballotlemimin  34669  ballotlemsgt1  34674  ballotlemsdom  34675  ballotlemsel1i  34676  ballotlemfrceq  34692  ballotlemfrcn0  34693  ballotlemirc  34695  ballotlem1ri  34698  fsum2dsub  34770  breprexplemc  34795  circlemeth  34803  erdszelem8  35399  poimirlem2  37960  poimirlem7  37965  poimirlem24  37982  poimirlem28  37986  fzsplitnd  42438  aks4d1p7d1  42538  aks4d1p7  42539  primrootspoweq0  42562  hashscontpow1  42577  aks6d1c5lem1  42592  aks6d1c5lem3  42593  aks6d1c5lem2  42594  unitscyglem2  42652  irrapxlem3  43273  fzmaxdif  43430  acongeq  43432  jm2.26  43451  monoords  45751  sumnnodd  46081  dvnprodlem1  46395  stoweidlem11  46460  stoweidlem26  46475  fourierdlem79  46634  elaa2lem  46682  etransclem1  46684  etransclem3  46686  etransclem7  46690  etransclem10  46693  etransclem15  46698  etransclem21  46704  etransclem22  46705  etransclem24  46707  etransclem25  46708  etransclem32  46715  etransclem35  46718  etransclem37  46720  etransclem38  46721  iccpartgtprec  47895