Theorem elfzelzd 13548

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

Syntax hints:   → wi 4   ∈ wcel 2143  (class class class)co 7410  ℤcz 12586  ...cfz 13530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  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 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7982  df-2nd 7983  df-neg 11439  df-z 12587  df-uz 12858  df-fz 13531

This theorem is referenced by:  fzone1  13809  seqf1olem1  14073  seqz  14082  seqcoll  14497  seqcoll2  14498  ccatswrd  14702  splfv1  14788  summolem2a  15762  fsumrev  15826  prodmolem2a  15984  fprod1p  16018  prmdivdiv  16841  4sqlem12  17011  pfxchn  18661  efgredleme  19808  efgredlemc  19810  efgredlemb  19811  wilthlem2  27233  lgsqrlem4  27513  lgsquadlem2  27545  pntlemj  27767  swrdrn2  33274  swrdrn3  33275  swrdf1  33276  gsummulsubdishift1  33388  cycpmco2lem7  33452  esplyindfv  33966  submateqlem2  34198  ballotlemimin  34896  ballotlemsgt1  34901  ballotlemsdom  34902  ballotlemsel1i  34903  ballotlemfrceq  34919  ballotlemfrcn0  34920  ballotlemirc  34922  ballotlem1ri  34925  fsum2dsub  34994  breprexplemc  35019  circlemeth  35027  erdszelem8  35690  poimirlem2  38293  poimirlem7  38298  poimirlem24  38315  poimirlem28  38319  fzsplitnd  42769  aks4d1p7d1  42869  aks4d1p7  42870  primrootspoweq0  42893  hashscontpow1  42908  aks6d1c5lem1  42923  aks6d1c5lem3  42924  aks6d1c5lem2  42925  unitscyglem2  42983  irrapxlem3  43571  fzmaxdif  43728  acongeq  43730  jm2.26  43749  monoords  46036  sumnnodd  46366  dvnprodlem1  46680  stoweidlem11  46745  stoweidlem26  46760  fourierdlem79  46919  elaa2lem  46967  etransclem1  46969  etransclem3  46971  etransclem7  46975  etransclem10  46978  etransclem15  46983  etransclem21  46989  etransclem22  46990  etransclem24  46992  etransclem25  46993  etransclem32  47000  etransclem35  47003  etransclem37  47005  etransclem38  47006  iccpartgtprec  48189