Theorem elfzelzd 13585

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7448  ℤcz 12639  ...cfz 13567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-neg 11523  df-z 12640  df-uz 12904  df-fz 13568

This theorem is referenced by:  seqf1olem1  14092  seqz  14101  seqcoll  14513  seqcoll2  14514  ccatswrd  14716  splfv1  14803  summolem2a  15763  fsumrev  15827  prodmolem2a  15982  fprod1p  16016  prmdivdiv  16834  4sqlem12  17003  efgredleme  19785  efgredlemc  19787  efgredlemb  19788  wilthlem2  27130  lgsqrlem4  27411  lgsquadlem2  27443  pntlemj  27665  fzone1  32805  swrdrn2  32921  swrdrn3  32922  swrdf1  32923  pfxchn  32982  cycpmco2lem7  33125  submateqlem2  33754  ballotlemimin  34470  ballotlemsgt1  34475  ballotlemsdom  34476  ballotlemsel1i  34477  ballotlemfrceq  34493  ballotlemfrcn0  34494  ballotlemirc  34496  ballotlem1ri  34499  fsum2dsub  34584  breprexplemc  34609  circlemeth  34617  erdszelem8  35166  poimirlem2  37582  poimirlem7  37587  poimirlem24  37604  poimirlem28  37608  fzsplitnd  41939  aks4d1p7d1  42039  aks4d1p7  42040  primrootspoweq0  42063  hashscontpow1  42078  aks6d1c5lem1  42093  aks6d1c5lem3  42094  aks6d1c5lem2  42095  unitscyglem2  42153  metakunt1  42162  metakunt3  42164  metakunt4  42165  metakunt7  42168  metakunt12  42173  metakunt21  42182  metakunt22  42183  metakunt27  42188  metakunt28  42189  metakunt29  42190  metakunt32  42193  irrapxlem3  42780  fzmaxdif  42938  acongeq  42940  jm2.26  42959  monoords  45212  sumnnodd  45551  dvnprodlem1  45867  stoweidlem11  45932  stoweidlem26  45947  fourierdlem79  46106  elaa2lem  46154  etransclem1  46156  etransclem3  46158  etransclem7  46162  etransclem10  46165  etransclem15  46170  etransclem21  46176  etransclem22  46177  etransclem24  46179  etransclem25  46180  etransclem32  46187  etransclem35  46190  etransclem37  46192  etransclem38  46193  iccpartgtprec  47294