Theorem elfzelzd 13530

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

Syntax hints:   → wi 4   ∈ wcel 2142  (class class class)co 7396  ℤcz 12568  ...cfz 13512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-1st 7970  df-2nd 7971  df-neg 11417  df-z 12569  df-uz 12840  df-fz 13513

This theorem is referenced by:  fzone1  13790  seqf1olem1  14054  seqz  14063  seqcoll  14477  seqcoll2  14478  ccatswrd  14682  splfv1  14768  summolem2a  15742  fsumrev  15806  prodmolem2a  15964  fprod1p  15998  prmdivdiv  16822  4sqlem12  16992  pfxchn  18642  efgredleme  19783  efgredlemc  19785  efgredlemb  19786  wilthlem2  27133  lgsqrlem4  27413  lgsquadlem2  27445  pntlemj  27667  swrdrn2  33132  swrdrn3  33133  swrdf1  33134  gsummulsubdishift1  33248  cycpmco2lem7  33312  esplyindfv  33873  submateqlem2  34105  ballotlemimin  34803  ballotlemsgt1  34808  ballotlemsdom  34809  ballotlemsel1i  34810  ballotlemfrceq  34826  ballotlemfrcn0  34827  ballotlemirc  34829  ballotlem1ri  34832  fsum2dsub  34901  breprexplemc  34926  circlemeth  34934  erdszelem8  35548  poimirlem2  38121  poimirlem7  38126  poimirlem24  38143  poimirlem28  38147  fzsplitnd  42599  aks4d1p7d1  42699  aks4d1p7  42700  primrootspoweq0  42723  hashscontpow1  42738  aks6d1c5lem1  42753  aks6d1c5lem3  42754  aks6d1c5lem2  42755  unitscyglem2  42813  irrapxlem3  43401  fzmaxdif  43558  acongeq  43560  jm2.26  43579  monoords  45876  sumnnodd  46206  dvnprodlem1  46520  stoweidlem11  46585  stoweidlem26  46600  fourierdlem79  46759  elaa2lem  46807  etransclem1  46809  etransclem3  46811  etransclem7  46815  etransclem10  46818  etransclem15  46823  etransclem21  46829  etransclem22  46830  etransclem24  46832  etransclem25  46833  etransclem32  46840  etransclem35  46843  etransclem37  46845  etransclem38  46846  iccpartgtprec  48026