Theorem elfzelz 13452

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 13448	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		eluzelz 12773	. 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ ℤ)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6500  (class class class)co 7368  ℤcz 12500  ℤ_≥cuz 12763  ...cfz 13435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944  df-neg 11379  df-z 12501  df-uz 12764  df-fz 13436

This theorem is referenced by:  elfzelzd  13453  fzssz  13454  elfz1eq  13463  fzsplit2  13477  fzdisj  13479  elfznn  13481  ssfzunsnext  13497  fznatpl1  13506  fzrev2i  13517  fzrev3i  13519  fznuz  13537  fzrevral  13540  fzshftral  13543  fznn0sub2  13563  elfzmlbm  13566  difelfznle  13570  predfz  13581  fzosplit  13620  sermono  13969  seqf1olem1  13976  seqf1olem2  13977  bcval2  14240  bcval4  14242  bccmpl  14244  bcp1nk  14252  bcval5  14253  bcpasc  14256  bccl2  14258  seqcoll2  14400  swrdval2  14582  swrdwrdsymb  14598  ccatpfx  14636  swrdswrd  14640  swrdpfx  14642  pfxccatin12lem2a  14662  pfxccatin12lem1  14663  swrdccatin2  14664  pfxccatin12lem2  14666  pfxccatin12  14668  spllen  14689  cshwidxm  14743  cshwidxn  14744  lswcshw  14750  2cshwcshw  14760  cshwcshid  14762  cshwcsh2id  14763  swrds2m  14876  seqshft  15020  sumrblem  15646  summolem2a  15650  fsum0diaglem  15711  mptfzshft  15713  fsumshftm  15716  fsum0diag2  15718  binomlem  15764  binom11  15767  bcxmas  15770  arisum  15795  geo2sum  15808  mertenslem1  15819  prodfn0  15829  prodrblem  15864  prodmolem2a  15869  fprodntriv  15877  fprodser  15884  fprodrev  15912  fallfacval3  15947  fallfacfwd  15971  0fallfac  15972  binomfallfaclem1  15974  binomfallfaclem2  15975  binomrisefac  15977  fallfacval4  15978  bpolycl  15987  bpolysum  15988  bpolydiflem  15989  fsumkthpow  15991  bpoly4  15994  fzm1ndvds  16261  pwp1fsum  16330  prmdvdsfz  16644  isprm7  16647  prmdvdsbc  16665  hashdvds  16714  phiprmpw  16715  prmdiveq  16725  modprminv  16739  modprminveq  16740  modprm0  16745  4sqlem11  16895  vdwapun  16914  prmop1  16978  prmdvdsprmo  16982  prmdvdsprmop  16983  prmgaplem1  16989  prmgaplem2  16990  prmgaplcmlem1  16991  prmgaplcmlem2  16992  prmgapprmo  17002  cshwshashlem1  17035  cshwshashlem2  17036  dfod2  19505  gsummptshft  19877  srgbinomlem3  20175  srgbinomlem4  20176  srgbinomlem  20177  freshmansdream  21541  chpscmatgsummon  22801  cayhamlem1  22822  iscmet3  25261  mbfi1fseqlem4  25687  itgz  25750  itgcl  25753  ibl0  25756  iblss  25774  iblss2  25775  itgss  25781  itgeqa  25783  iblconst  25787  iblabsr  25799  iblmulc2  25800  itgsplit  25805  dvfsumlem3  26003  plyeq0lem  26183  aalioulem1  26308  cxpeq  26735  birthdaylem2  26930  wilthlem1  27046  wilthlem3  27048  ftalem5  27055  basellem3  27061  basellem4  27062  dvdsppwf1o  27164  dvdsflf1o  27165  musum  27169  ppiub  27183  chtublem  27190  mersenne  27206  bposlem1  27263  lgsval2lem  27286  lgsdilem2  27312  lgsqrlem2  27326  gausslemma2dlem1a  27344  gausslemma2dlem1  27345  gausslemma2dlem3  27347  gausslemma2dlem4  27348  gausslemma2dlem5a  27349  gausslemma2dlem5  27350  gausslemma2dlem6  27351  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  2lgslem1a1  27368  2lgslem1a  27370  2lgslem1b  27371  rpvmasumlem  27466  dchrisumlem1  27468  dchrisumlem2  27469  dchrmusum2  27473  dchrvmasumlem1  27474  dchrvmasum2lem  27475  dchrvmasum2if  27476  dchrvmasumlem3  27478  dchrvmasumiflem1  27480  dchrvmasumiflem2  27481  dchrisum0flblem1  27487  rpvmasum2  27491  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2a  27496  dchrisum0lem2  27497  dchrisum0lem3  27498  dchrmusumlem  27501  dchrvmasumlem  27502  logdivbnd  27535  pntpbnd1  27565  pntlemh  27578  pntlemf  27584  ostth2lem2  27613  axlowdimlem13  29039  axlowdimlem14  29040  axlowdimlem16  29042  crctcshlem4  29905  crctcshwlkn0  29906  erclwwlkeqlen  30106  clwwnisshclwwsn  30146  eleclclwwlknlem2  30148  erclwwlkneqlen  30155  fzm1ne1  32879  fzsplit3  32884  bcm1n  32886  ballotlemfc0  34671  ballotlemfcc  34672  ballotlemodife  34676  ballotlemimin  34684  ballotlemsgt1  34689  ballotlemsel1i  34691  ballotlemsf1o  34692  ballotlemsi  34693  ballotlemsima  34694  ballotlemfg  34704  ballotlemfrc  34705  ballotlemfrcn0  34708  revpfxsfxrev  35332  swrdrevpfx  35333  pfxwlk  35340  swrdwlk  35343  erdszelem8  35414  erdszelem9  35415  cvmliftlem7  35507  supfz  35945  inffz  35946  bcprod  35954  fwddifnp1  36381  poimirlem1  37872  poimirlem14  37885  poimirlem15  37886  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem23  37894  poimirlem24  37895  poimirlem27  37898  poimirlem31  37902  poimirlem32  37903  mblfinlem2  37909  iblmulc2nc  37936  fdc  37996  lcmineqlem1  42399  lcmineqlem6  42404  lcmineqlem17  42415  aks4d1p1p1  42433  aks6d1c1  42486  hashscontpow  42492  aks6d1c5lem0  42505  aks6d1c5lem3  42507  aks6d1c5  42509  sticksstones6  42521  sticksstones7  42522  sticksstones10  42525  sticksstones12a  42527  sticksstones12  42528  aks6d1c6lem1  42540  bcled  42548  bcle2d  42549  aks5lem5a  42561  grpods  42564  unitscyglem2  42566  unitscyglem4  42568  sumcubes  42683  irrapxlem1  43179  irrapxlem2  43180  irrapxlem3  43181  pellexlem5  43190  acongrep  43337  acongeq  43340  jm2.22  43352  jm2.23  43353  jm2.26lem3  43358  jm2.27dlem2  43367  hashnzfz  44676  monoords  45659  fmul01lt1lem1  45944  fmul01lt1lem2  45945  sumnnodd  45990  limsupubuzlem  46070  dvnmul  46301  dvnprodlem1  46304  dvnprodlem2  46305  iblsplit  46324  iblspltprt  46331  itgspltprt  46337  stoweidlem3  46361  stoweidlem11  46369  stoweidlem20  46378  stoweidlem26  46384  stoweidlem34  46392  stoweidlem59  46417  stirlinglem10  46441  dirkertrigeqlem1  46456  dirkertrigeqlem2  46457  dirkertrigeqlem3  46458  dirkertrigeq  46459  dirkeritg  46460  fourierdlem11  46476  fourierdlem12  46477  fourierdlem15  46480  fourierdlem34  46499  fourierdlem41  46506  fourierdlem46  46510  fourierdlem48  46512  fourierdlem49  46513  fourierdlem50  46514  fourierdlem54  46518  fourierdlem63  46527  fourierdlem64  46528  fourierdlem65  46529  fourierdlem79  46543  fourierdlem102  46566  fourierdlem103  46567  fourierdlem104  46568  fourierdlem114  46578  elaa2lem  46591  etransclem4  46596  etransclem7  46599  etransclem8  46600  etransclem17  46609  etransclem18  46610  etransclem20  46612  etransclem23  46615  etransclem27  46619  etransclem31  46623  etransclem32  46624  etransclem35  46627  etransclem41  46633  etransclem46  46638  etransclem48  46640  iundjiun  46818  caratheodorylem1  46884  2elfz2melfz  47678  elfzelfzlble  47681  el1fzopredsuc  47685  iccpartiltu  47782  iccpartgt  47787  iccpartnel  47798  fargshiftfo  47802  altgsumbc  48712  altgsumbcALT  48713  nn0sumshdiglemA  48979  nn0sumshdiglemB  48980