Theorem elfzelzd 13667

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7427  ℤcz 12703  ...cfz 13649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pr 5394  ax-un 7758  ax-cnex 11266  ax-resscn 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-fv 6554  df-ov 7430  df-oprab 7431  df-mpo 7432  df-1st 8008  df-2nd 8009  df-neg 11554  df-z 12704  df-uz 12976  df-fz 13650

This theorem is used by:  fzone1  13929  seqf1olem1  14194  seqz  14203  seqcoll  14619  seqcoll2  14620  swrdf1  14810  swrdrn3  14813  ccatswrd  14829  splfv1  14915  summolem2a  15893  fsumrev  15957  prodmolem2a  16113  fprod1p  16147  prmdivdiv  16976  4sqlem12  17146  pfxchn  18796  efgredleme  19969  efgredlemc  19971  efgredlemb  19972  wilthlem2  27408  lgsqrlem4  27688  lgsquadlem2  27720  pntlemj  27942  swrdrn2  33570  gsummulsubdishift1  33682  cycpmco2lem7  33746  esplyindfv  34261  submateqlem2  34493  ballotlemimin  35191  ballotlemsgt1  35196  ballotlemsdom  35197  ballotlemsel1i  35198  ballotlemfrceq  35214  ballotlemfrcn0  35215  ballotlemirc  35217  ballotlem1ri  35220  fsum2dsub  35289  breprexplemc  35314  circlemeth  35322  erdszelem8  36084  poimirlem2  38680  poimirlem7  38685  poimirlem24  38702  poimirlem28  38706  fzsplitnd  43172  aks4d1p7d1  43272  aks4d1p7  43273  primrootspoweq0  43296  hashscontpow1  43311  aks6d1c5lem1  43326  aks6d1c5lem3  43327  aks6d1c5lem2  43328  unitscyglem2  43386  irrapxlem3  43971  fzmaxdif  44128  acongeq  44130  jm2.26  44149  monoords  46452  sumnnodd  46781  dvnprodlem1  47095  stoweidlem11  47160  stoweidlem26  47175  fourierdlem79  47334  elaa2lem  47382  etransclem1  47384  etransclem3  47386  etransclem7  47390  etransclem10  47393  etransclem15  47398  etransclem21  47404  etransclem22  47405  etransclem24  47407  etransclem25  47408  etransclem32  47415  etransclem35  47418  etransclem37  47420  etransclem38  47421  iccpartgtprec  48641