Theorem elfzelz 13564

Description: A member of a finite set of sequential integers is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzelz	⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

Proof of Theorem elfzelz

Step	Hyp	Ref	Expression
1		elfzuz 13560	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		eluzelz 12884	. 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ ℤ)
3	1, 2	syl 18	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ‘cfv 6540  (class class class)co 7416  ℤcz 12602  ℤ_≥cuz 12874  ...cfz 13547

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7738  ax-cnex 11167  ax-resscn 11168

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7419  df-oprab 7420  df-mpo 7421  df-1st 7988  df-2nd 7989  df-neg 11455  df-z 12603  df-uz 12875  df-fz 13548

This theorem is used by:  elfzelzd  13565  fzssz  13566  elfz1eq  13575  fzsplit2  13590  fzdisj  13592  elfznn  13594  ssfzunsnext  13610  fznatpl1  13619  fzrev2i  13630  fzrev3i  13632  fznuz  13650  fzrevral  13653  fzshftral  13656  fznn0sub2  13676  elfzmlbm  13679  difelfznle  13683  predfz  13694  fzosplit  13734  sermono  14084  seqf1olem1  14091  seqf1olem2  14092  bcval2  14355  bcval4  14357  bccmpl  14359  bcp1nk  14367  bcval5  14368  bcpasc  14371  bccl2  14373  seqcoll2  14516  swrdval2  14700  swrdwrdsymb  14718  ccatpfx  14756  swrdswrd  14760  swrdpfx  14762  pfxccatin12lem2a  14782  pfxccatin12lem1  14783  swrdccatin2  14784  pfxccatin12lem2  14786  pfxccatin12  14788  spllen  14809  revpfxsfxrev  14823  swrdrevpfx  14824  cshwidxm  14865  cshwidxn  14866  lswcshw  14872  2cshwcshw  14882  cshwcshid  14884  cshwcsh2id  14885  swrds2m  14998  seqshft  15142  sumrblem  15781  summolem2a  15785  fsum0diaglem  15846  mptfzshft  15848  fsumshftm  15851  fsum0diag2  15853  binomlem  15902  binom11  15905  bcxmas  15908  arisum  15933  geo2sum  15946  mertenslem1  15957  prodfn0  15967  prodrblem  16002  prodmolem2a  16007  fprodntriv  16015  fprodser  16022  fprodrev  16050  fallfacval3  16085  fallfacfwd  16108  0fallfac  16109  binomfallfaclem1  16111  binomfallfaclem2  16112  binomrisefac  16114  fallfacval4  16115  bpolycl  16124  bpolysum  16125  bpolydiflem  16126  fsumkthpow  16128  bpoly4  16131  fzm1ndvds  16398  pwp1fsum  16467  prmdvdsfz  16782  isprm7  16785  prmdvdsbc  16803  hashdvds  16852  phiprmpw  16853  prmdiveq  16863  modprminv  16877  modprminveq  16878  modprm0  16883  4sqlem11  17033  vdwapun  17052  prmop1  17116  prmdvdsprmo  17120  prmdvdsprmop  17121  prmgaplem1  17127  prmgaplem2  17128  prmgaplcmlem1  17129  prmgaplcmlem2  17130  prmgapprmo  17140  cshwshashlem1  17173  cshwshashlem2  17174  dfod2  19658  gsummptshft  20030  srgbinomlem3  20334  srgbinomlem4  20335  srgbinomlem  20336  freshmansdream  21754  chpscmatgsummon  23032  cayhamlem1  23053  iscmet3  25483  mbfi1fseqlem4  25908  itgz  25971  itgcl  25974  ibl0  25977  iblss  25995  iblss2  25996  itgss  26002  itgeqa  26004  iblconst  26008  iblabsr  26020  iblmulc2  26021  itgsplit  26026  dvfsumlem3  26218  plyeq0lem  26398  aalioulem1  26526  cxpeq  26953  birthdaylem2  27148  wilthlem1  27263  wilthlem3  27265  ftalem5  27272  basellem3  27278  basellem4  27279  dvdsppwf1o  27381  dvdsflf1o  27382  musum  27386  ppiub  27399  chtublem  27406  mersenne  27422  bposlem1  27479  lgsval2lem  27502  lgsdilem2  27528  lgsqrlem2  27542  gausslemma2dlem1a  27560  gausslemma2dlem1  27561  gausslemma2dlem3  27563  gausslemma2dlem4  27564  gausslemma2dlem5a  27565  gausslemma2dlem5  27566  gausslemma2dlem6  27567  lgseisenlem1  27570  lgseisenlem2  27571  lgseisenlem3  27572  lgsquadlem1  27575  lgsquadlem2  27576  lgsquadlem3  27577  2lgslem1a1  27584  2lgslem1a  27586  2lgslem1b  27587  rpvmasumlem  27682  dchrisumlem1  27684  dchrisumlem2  27685  dchrmusum2  27689  dchrvmasumlem1  27690  dchrvmasum2lem  27691  dchrvmasum2if  27692  dchrvmasumlem3  27694  dchrvmasumiflem1  27696  dchrvmasumiflem2  27697  dchrisum0flblem1  27703  rpvmasum2  27707  dchrisum0lem1b  27710  dchrisum0lem1  27711  dchrisum0lem2a  27712  dchrisum0lem2  27713  dchrisum0lem3  27714  dchrmusumlem  27717  dchrvmasumlem  27718  logdivbnd  27751  pntpbnd1  27781  pntlemh  27794  pntlemf  27800  ostth2lem2  27829  axlowdimlem13  29335  axlowdimlem14  29336  axlowdimlem16  29338  pfxwlk  30069  swrdwlk  30071  crctcshlem4  30212  crctcshwlkn0  30213  erclwwlkeqlen  30413  clwwnisshclwwsn  30453  eleclclwwlknlem2  30455  erclwwlkneqlen  30462  fzm1ne1  33179  fzsplit3  33184  bcm1n  33186  ballotlemfc0  34924  ballotlemfcc  34925  ballotlemodife  34929  ballotlemimin  34937  ballotlemsgt1  34942  ballotlemsel1i  34944  ballotlemsf1o  34945  ballotlemsi  34946  ballotlemsima  34947  ballotlemfg  34957  ballotlemfrc  34958  ballotlemfrcn0  34961  erdszelem8  35703  erdszelem9  35704  cvmliftlem7  35796  supfz  36234  inffz  36235  bcprod  36243  fwddifnp1  36670  poimirlem1  38305  poimirlem14  38318  poimirlem15  38319  poimirlem16  38320  poimirlem17  38321  poimirlem19  38323  poimirlem20  38324  poimirlem23  38327  poimirlem24  38328  poimirlem27  38331  poimirlem31  38335  poimirlem32  38336  mblfinlem2  38342  iblmulc2nc  38369  fdc  38429  lcmineqlem1  42829  lcmineqlem6  42834  lcmineqlem17  42845  aks4d1p1p1  42863  aks6d1c1  42916  hashscontpow  42922  aks6d1c5lem0  42935  aks6d1c5lem3  42937  aks6d1c5  42939  sticksstones6  42951  sticksstones7  42952  sticksstones10  42955  sticksstones12a  42957  sticksstones12  42958  aks6d1c6lem1  42970  bcled  42978  bcle2d  42979  aks5lem5a  42991  grpods  42994  unitscyglem2  42996  unitscyglem4  42998  sumcubes  43107  irrapxlem1  43582  irrapxlem2  43583  irrapxlem3  43584  pellexlem5  43593  acongrep  43740  acongeq  43743  jm2.22  43755  jm2.23  43756  jm2.26lem3  43761  jm2.27dlem2  43770  hashnzfz  45063  monoords  46049  fmul01lt1lem1  46333  fmul01lt1lem2  46334  sumnnodd  46379  limsupubuzlem  46459  dvnmul  46690  dvnprodlem1  46693  dvnprodlem2  46694  iblsplit  46713  iblspltprt  46720  itgspltprt  46726  stoweidlem3  46750  stoweidlem11  46758  stoweidlem20  46767  stoweidlem26  46773  stoweidlem34  46781  stoweidlem59  46806  stirlinglem10  46830  dirkertrigeqlem1  46845  dirkertrigeqlem2  46846  dirkertrigeqlem3  46847  dirkertrigeq  46848  dirkeritg  46849  fourierdlem11  46865  fourierdlem12  46866  fourierdlem15  46869  fourierdlem34  46888  fourierdlem41  46895  fourierdlem46  46899  fourierdlem48  46901  fourierdlem49  46902  fourierdlem50  46903  fourierdlem54  46907  fourierdlem63  46916  fourierdlem64  46917  fourierdlem65  46918  fourierdlem79  46932  fourierdlem102  46955  fourierdlem103  46956  fourierdlem104  46957  fourierdlem114  46967  elaa2lem  46980  etransclem4  46985  etransclem7  46988  etransclem8  46989  etransclem17  46998  etransclem18  46999  etransclem20  47001  etransclem23  47004  etransclem27  47008  etransclem31  47012  etransclem32  47013  etransclem35  47016  etransclem41  47022  etransclem46  47027  etransclem48  47029  iundjiun  47207  caratheodorylem1  47273  2elfz2melfz  48088  elfzelfzlble  48091  el1fzopredsuc  48096  iccpartiltu  48204  iccpartgt  48209  iccpartnel  48220  fargshiftfo  48224  altgsumbc  49165  altgsumbcALT  49166  nn0sumshdiglemA  49432  nn0sumshdiglemB  49433