Theorem elfzelz 13419

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

Syntax hints:   → wi 4   ∈ wcel 2111  ‘cfv 6476  (class class class)co 7341  ℤcz 12463  ℤ_≥cuz 12727  ...cfz 13402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663  ax-cnex 11057  ax-resscn 11058

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-fv 6484  df-ov 7344  df-oprab 7345  df-mpo 7346  df-1st 7916  df-2nd 7917  df-neg 11342  df-z 12464  df-uz 12728  df-fz 13403

This theorem is referenced by:  elfzelzd  13420  fzssz  13421  elfz1eq  13430  fzsplit2  13444  fzdisj  13446  elfznn  13448  ssfzunsnext  13464  fznatpl1  13473  fzrev2i  13484  fzrev3i  13486  fznuz  13504  fzrevral  13507  fzshftral  13510  fznn0sub2  13530  elfzmlbm  13533  difelfznle  13537  predfz  13548  fzosplit  13587  sermono  13936  seqf1olem1  13943  seqf1olem2  13944  bcval2  14207  bcval4  14209  bccmpl  14211  bcp1nk  14219  bcval5  14220  bcpasc  14223  bccl2  14225  seqcoll2  14367  swrdval2  14549  swrdwrdsymb  14565  ccatpfx  14603  swrdswrd  14607  swrdpfx  14609  pfxccatin12lem2a  14629  pfxccatin12lem1  14630  swrdccatin2  14631  pfxccatin12lem2  14633  pfxccatin12  14635  spllen  14656  cshwidxm  14710  cshwidxn  14711  lswcshw  14717  2cshwcshw  14727  cshwcshid  14729  cshwcsh2id  14730  swrds2m  14843  seqshft  14987  sumrblem  15613  summolem2a  15617  fsum0diaglem  15678  mptfzshft  15680  fsumshftm  15683  fsum0diag2  15685  binomlem  15731  binom11  15734  bcxmas  15737  arisum  15762  geo2sum  15775  mertenslem1  15786  prodfn0  15796  prodrblem  15831  prodmolem2a  15836  fprodntriv  15844  fprodser  15851  fprodrev  15879  fallfacval3  15914  fallfacfwd  15938  0fallfac  15939  binomfallfaclem1  15941  binomfallfaclem2  15942  binomrisefac  15944  fallfacval4  15945  bpolycl  15954  bpolysum  15955  bpolydiflem  15956  fsumkthpow  15958  bpoly4  15961  fzm1ndvds  16228  pwp1fsum  16297  prmdvdsfz  16611  isprm7  16614  prmdvdsbc  16632  hashdvds  16681  phiprmpw  16682  prmdiveq  16692  modprminv  16706  modprminveq  16707  modprm0  16712  4sqlem11  16862  vdwapun  16881  prmop1  16945  prmdvdsprmo  16949  prmdvdsprmop  16950  prmgaplem1  16956  prmgaplem2  16957  prmgaplcmlem1  16958  prmgaplcmlem2  16959  prmgapprmo  16969  cshwshashlem1  17002  cshwshashlem2  17003  dfod2  19471  gsummptshft  19843  srgbinomlem3  20141  srgbinomlem4  20142  srgbinomlem  20143  freshmansdream  21506  chpscmatgsummon  22755  cayhamlem1  22776  iscmet3  25215  mbfi1fseqlem4  25641  itgz  25704  itgcl  25707  ibl0  25710  iblss  25728  iblss2  25729  itgss  25735  itgeqa  25737  iblconst  25741  iblabsr  25753  iblmulc2  25754  itgsplit  25759  dvfsumlem3  25957  plyeq0lem  26137  aalioulem1  26262  cxpeq  26689  birthdaylem2  26884  wilthlem1  27000  wilthlem3  27002  ftalem5  27009  basellem3  27015  basellem4  27016  dvdsppwf1o  27118  dvdsflf1o  27119  musum  27123  ppiub  27137  chtublem  27144  mersenne  27160  bposlem1  27217  lgsval2lem  27240  lgsdilem2  27266  lgsqrlem2  27280  gausslemma2dlem1a  27298  gausslemma2dlem1  27299  gausslemma2dlem3  27301  gausslemma2dlem4  27302  gausslemma2dlem5a  27303  gausslemma2dlem5  27304  gausslemma2dlem6  27305  lgseisenlem1  27308  lgseisenlem2  27309  lgseisenlem3  27310  lgsquadlem1  27313  lgsquadlem2  27314  lgsquadlem3  27315  2lgslem1a1  27322  2lgslem1a  27324  2lgslem1b  27325  rpvmasumlem  27420  dchrisumlem1  27422  dchrisumlem2  27423  dchrmusum2  27427  dchrvmasumlem1  27428  dchrvmasum2lem  27429  dchrvmasum2if  27430  dchrvmasumlem3  27432  dchrvmasumiflem1  27434  dchrvmasumiflem2  27435  dchrisum0flblem1  27441  rpvmasum2  27445  dchrisum0lem1b  27448  dchrisum0lem1  27449  dchrisum0lem2a  27450  dchrisum0lem2  27451  dchrisum0lem3  27452  dchrmusumlem  27455  dchrvmasumlem  27456  logdivbnd  27489  pntpbnd1  27519  pntlemh  27532  pntlemf  27538  ostth2lem2  27567  axlowdimlem13  28927  axlowdimlem14  28928  axlowdimlem16  28930  crctcshlem4  29793  crctcshwlkn0  29794  erclwwlkeqlen  29991  clwwnisshclwwsn  30031  eleclclwwlknlem2  30033  erclwwlkneqlen  30040  fzm1ne1  32763  fzsplit3  32768  bcm1n  32769  ballotlemfc0  34498  ballotlemfcc  34499  ballotlemodife  34503  ballotlemimin  34511  ballotlemsgt1  34516  ballotlemsel1i  34518  ballotlemsf1o  34519  ballotlemsi  34520  ballotlemsima  34521  ballotlemfg  34531  ballotlemfrc  34532  ballotlemfrcn0  34535  revpfxsfxrev  35152  swrdrevpfx  35153  pfxwlk  35160  swrdwlk  35163  erdszelem8  35234  erdszelem9  35235  cvmliftlem7  35327  supfz  35765  inffz  35766  bcprod  35774  fwddifnp1  36199  poimirlem1  37661  poimirlem14  37674  poimirlem15  37675  poimirlem16  37676  poimirlem17  37677  poimirlem19  37679  poimirlem20  37680  poimirlem23  37683  poimirlem24  37684  poimirlem27  37687  poimirlem31  37691  poimirlem32  37692  mblfinlem2  37698  iblmulc2nc  37725  fdc  37785  lcmineqlem1  42062  lcmineqlem6  42067  lcmineqlem17  42078  aks4d1p1p1  42096  aks6d1c1  42149  hashscontpow  42155  aks6d1c5lem0  42168  aks6d1c5lem3  42170  aks6d1c5  42172  sticksstones6  42184  sticksstones7  42185  sticksstones10  42188  sticksstones12a  42190  sticksstones12  42191  aks6d1c6lem1  42203  bcled  42211  bcle2d  42212  aks5lem5a  42224  grpods  42227  unitscyglem2  42229  unitscyglem4  42231  sumcubes  42346  irrapxlem1  42855  irrapxlem2  42856  irrapxlem3  42857  pellexlem5  42866  acongrep  43013  acongeq  43016  jm2.22  43028  jm2.23  43029  jm2.26lem3  43034  jm2.27dlem2  43043  hashnzfz  44353  monoords  45338  fmul01lt1lem1  45624  fmul01lt1lem2  45625  sumnnodd  45670  limsupubuzlem  45750  dvnmul  45981  dvnprodlem1  45984  dvnprodlem2  45985  iblsplit  46004  iblspltprt  46011  itgspltprt  46017  stoweidlem3  46041  stoweidlem11  46049  stoweidlem20  46058  stoweidlem26  46064  stoweidlem34  46072  stoweidlem59  46097  stirlinglem10  46121  dirkertrigeqlem1  46136  dirkertrigeqlem2  46137  dirkertrigeqlem3  46138  dirkertrigeq  46139  dirkeritg  46140  fourierdlem11  46156  fourierdlem12  46157  fourierdlem15  46160  fourierdlem34  46179  fourierdlem41  46186  fourierdlem46  46190  fourierdlem48  46192  fourierdlem49  46193  fourierdlem50  46194  fourierdlem54  46198  fourierdlem63  46207  fourierdlem64  46208  fourierdlem65  46209  fourierdlem79  46223  fourierdlem102  46246  fourierdlem103  46247  fourierdlem104  46248  fourierdlem114  46258  elaa2lem  46271  etransclem4  46276  etransclem7  46279  etransclem8  46280  etransclem17  46289  etransclem18  46290  etransclem20  46292  etransclem23  46295  etransclem27  46299  etransclem31  46303  etransclem32  46304  etransclem35  46307  etransclem41  46313  etransclem46  46318  etransclem48  46320  iundjiun  46498  caratheodorylem1  46564  2elfz2melfz  47349  elfzelfzlble  47352  el1fzopredsuc  47356  iccpartiltu  47453  iccpartgt  47458  iccpartnel  47469  fargshiftfo  47473  altgsumbc  48383  altgsumbcALT  48384  nn0sumshdiglemA  48651  nn0sumshdiglemB  48652