Theorem elfzelzd 13553

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

Syntax hints:   → wi 4   ∈ wcel 2149  (class class class)co 7411  ℤcz 12591  ...cfz 13535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-resscn 11157

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7986  df-2nd 7987  df-neg 11444  df-z 12592  df-uz 12863  df-fz 13536

This theorem is referenced by:  fzone1  13813  seqf1olem1  14077  seqz  14086  seqcoll  14501  seqcoll2  14502  ccatswrd  14706  splfv1  14792  summolem2a  15766  fsumrev  15830  prodmolem2a  15988  fprod1p  16022  prmdivdiv  16846  4sqlem12  17016  pfxchn  18666  efgredleme  19813  efgredlemc  19815  efgredlemb  19816  wilthlem2  27199  lgsqrlem4  27479  lgsquadlem2  27511  pntlemj  27733  swrdrn2  33215  swrdrn3  33216  swrdf1  33217  gsummulsubdishift1  33329  cycpmco2lem7  33393  esplyindfv  33911  submateqlem2  34143  ballotlemimin  34841  ballotlemsgt1  34846  ballotlemsdom  34847  ballotlemsel1i  34848  ballotlemfrceq  34864  ballotlemfrcn0  34865  ballotlemirc  34867  ballotlem1ri  34870  fsum2dsub  34939  breprexplemc  34964  circlemeth  34972  erdszelem8  35589  poimirlem2  38161  poimirlem7  38166  poimirlem24  38183  poimirlem28  38187  fzsplitnd  42639  aks4d1p7d1  42739  aks4d1p7  42740  primrootspoweq0  42763  hashscontpow1  42778  aks6d1c5lem1  42793  aks6d1c5lem3  42794  aks6d1c5lem2  42795  unitscyglem2  42853  irrapxlem3  43443  fzmaxdif  43600  acongeq  43602  jm2.26  43621  monoords  45908  sumnnodd  46238  dvnprodlem1  46552  stoweidlem11  46617  stoweidlem26  46632  fourierdlem79  46791  elaa2lem  46839  etransclem1  46841  etransclem3  46843  etransclem7  46847  etransclem10  46850  etransclem15  46855  etransclem21  46861  etransclem22  46862  etransclem24  46864  etransclem25  46865  etransclem32  46872  etransclem35  46875  etransclem37  46877  etransclem38  46878  iccpartgtprec  48058