Theorem elfzelz 12961

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

Syntax hints:   → wi 4   ∈ wcel 2111  ‘cfv 6339  (class class class)co 7155  ℤcz 12025  ℤ_≥cuz 12287  ...cfz 12944

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301  ax-un 7464  ax-cnex 10636  ax-resscn 10637

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-iun 4888  df-br 5036  df-opab 5098  df-mpt 5116  df-id 5433  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-fv 6347  df-ov 7158  df-oprab 7159  df-mpo 7160  df-1st 7698  df-2nd 7699  df-neg 10916  df-z 12026  df-uz 12288  df-fz 12945

This theorem is referenced by:  elfzelzd  12962  fzssz  12963  elfz1eq  12972  fzsplit2  12986  fzdisj  12988  elfznn  12990  ssfzunsnext  13006  fznatpl1  13015  fzrev2i  13026  fzrev3i  13028  fznuz  13043  fzrevral  13046  fzshftral  13049  fznn0sub2  13068  elfzmlbm  13071  difelfznle  13075  predfz  13086  fzosplit  13124  sermono  13457  seqf1olem1  13464  seqf1olem2  13465  bcval2  13720  bcval4  13722  bccmpl  13724  bcp1nk  13732  bcval5  13733  bcpasc  13736  bccl2  13738  seqcoll  13879  seqcoll2  13880  swrdval2  14060  swrdwrdsymb  14076  ccatswrd  14082  addlenrevpfx  14104  ccatpfx  14115  swrdswrd  14119  swrdpfx  14121  pfxccatin12lem2a  14141  pfxccatin12lem1  14142  swrdccatin2  14143  pfxccatin12lem2  14145  pfxccatin12  14147  spllen  14168  splfv1  14169  cshwidxm  14222  cshwidxn  14223  lswcshw  14229  2cshwcshw  14239  cshwcshid  14241  cshwcsh2id  14242  swrds2m  14355  seqshft  14497  sumrblem  15121  summolem2a  15125  fsum0diaglem  15184  mptfzshft  15186  fsumrev  15187  fsumshftm  15189  fsum0diag2  15191  binomlem  15237  binom11  15240  bcxmas  15243  arisum  15268  geo2sum  15282  mertenslem1  15293  prodfn0  15303  prodrblem  15336  prodmolem2a  15341  fprodntriv  15349  fprodser  15356  fprod1p  15375  fprodrev  15384  fallfacval3  15419  fallfacfwd  15443  0fallfac  15444  binomfallfaclem1  15446  binomfallfaclem2  15447  binomrisefac  15449  fallfacval4  15450  bpolycl  15459  bpolysum  15460  bpolydiflem  15461  fsumkthpow  15463  bpoly4  15466  fzm1ndvds  15728  pwp1fsum  15797  prmdvdsfz  16106  isprm7  16109  hashdvds  16172  phiprmpw  16173  prmdiveq  16183  prmdivdiv  16184  modprminv  16196  modprminveq  16197  modprm0  16202  4sqlem11  16351  4sqlem12  16352  vdwapun  16370  prmop1  16434  prmdvdsprmo  16438  prmdvdsprmop  16439  prmgaplem1  16445  prmgaplem2  16446  prmgaplcmlem1  16447  prmgaplcmlem2  16448  prmgapprmo  16458  cshwshashlem1  16492  cshwshashlem2  16493  dfod2  18763  efgredleme  18941  efgredlemc  18943  efgredlemb  18944  gsummptshft  19129  srgbinomlem3  19365  srgbinomlem4  19366  srgbinomlem  19367  chpscmatgsummon  21550  cayhamlem1  21571  iscmet3  23998  mbfi1fseqlem4  24423  itgz  24485  itgcl  24488  ibl0  24491  iblss  24509  iblss2  24510  itgss  24516  itgeqa  24518  iblconst  24522  iblabsr  24534  iblmulc2  24535  itgsplit  24540  dvfsumlem3  24732  plyeq0lem  24911  aalioulem1  25032  cxpeq  25450  birthdaylem2  25642  wilthlem1  25757  wilthlem2  25758  wilthlem3  25759  ftalem5  25766  basellem3  25772  basellem4  25773  dvdsppwf1o  25875  dvdsflf1o  25876  musum  25880  ppiub  25892  chtublem  25899  mersenne  25915  bposlem1  25972  lgsval2lem  25995  lgsdilem2  26021  lgsqrlem2  26035  lgsqrlem4  26037  gausslemma2dlem1a  26053  gausslemma2dlem1  26054  gausslemma2dlem3  26056  gausslemma2dlem4  26057  gausslemma2dlem5a  26058  gausslemma2dlem5  26059  gausslemma2dlem6  26060  lgseisenlem1  26063  lgseisenlem2  26064  lgseisenlem3  26065  lgsquadlem1  26068  lgsquadlem2  26069  lgsquadlem3  26070  2lgslem1a1  26077  2lgslem1a  26079  2lgslem1b  26080  rpvmasumlem  26175  dchrisumlem1  26177  dchrisumlem2  26178  dchrmusum2  26182  dchrvmasumlem1  26183  dchrvmasum2lem  26184  dchrvmasum2if  26185  dchrvmasumlem3  26187  dchrvmasumiflem1  26189  dchrvmasumiflem2  26190  dchrisum0flblem1  26196  rpvmasum2  26200  dchrisum0lem1b  26203  dchrisum0lem1  26204  dchrisum0lem2a  26205  dchrisum0lem2  26206  dchrisum0lem3  26207  dchrmusumlem  26210  dchrvmasumlem  26211  logdivbnd  26244  pntpbnd1  26274  pntlemh  26287  pntlemj  26291  pntlemf  26293  ostth2lem2  26322  axlowdimlem13  26852  axlowdimlem14  26853  axlowdimlem16  26855  crctcshlem4  27710  crctcshwlkn0  27711  erclwwlkeqlen  27908  clwwnisshclwwsn  27948  eleclclwwlknlem2  27950  erclwwlkneqlen  27957  fzm1ne1  30638  fzsplit3  30643  bcm1n  30644  fzone1  30649  prmdvdsbc  30658  swrdf1  30756  cycpmco2lem7  30929  freshmansdream  31014  ballotlemfc0  31982  ballotlemfcc  31983  ballotlemodife  31987  ballotlemimin  31995  ballotlemsgt1  32000  ballotlemsel1i  32002  ballotlemsf1o  32003  ballotlemsi  32004  ballotlemsima  32005  ballotlemfg  32015  ballotlemfrc  32016  ballotlemfrceq  32018  ballotlemfrcn0  32019  ballotlemirc  32021  ballotlem1ri  32024  revpfxsfxrev  32597  swrdrevpfx  32598  pfxwlk  32605  swrdwlk  32608  erdszelem8  32680  erdszelem9  32681  cvmliftlem7  32773  supfz  33213  inffz  33214  bcprod  33223  fwddifnp1  34042  poimirlem1  35364  poimirlem2  35365  poimirlem7  35370  poimirlem14  35377  poimirlem15  35378  poimirlem16  35379  poimirlem17  35380  poimirlem19  35382  poimirlem20  35383  poimirlem23  35386  poimirlem24  35387  poimirlem27  35390  poimirlem28  35391  poimirlem31  35394  poimirlem32  35395  mblfinlem2  35401  iblmulc2nc  35428  fdc  35489  lcmineqlem1  39622  lcmineqlem6  39627  lcmineqlem17  39638  aks4d1p1p1  39655  metakunt15  39687  metakunt16  39688  metakunt19  39691  metakunt25  39697  metakunt33  39705  irrapxlem1  40164  irrapxlem2  40165  irrapxlem3  40166  pellexlem5  40175  acongrep  40322  fzmaxdif  40323  acongeq  40325  jm2.22  40337  jm2.23  40338  jm2.26lem3  40343  jm2.26  40344  jm2.27dlem2  40352  hashnzfz  41425  monoords  42325  fmul01lt1lem1  42620  fmul01lt1lem2  42621  sumnnodd  42666  limsupubuzlem  42748  dvnmul  42979  dvnprodlem2  42983  iblsplit  43002  iblspltprt  43009  itgspltprt  43015  stoweidlem3  43039  stoweidlem11  43047  stoweidlem20  43056  stoweidlem26  43062  stoweidlem34  43070  stoweidlem59  43095  stirlinglem10  43119  dirkertrigeqlem1  43134  dirkertrigeqlem2  43135  dirkertrigeqlem3  43136  dirkertrigeq  43137  dirkeritg  43138  fourierdlem11  43154  fourierdlem12  43155  fourierdlem15  43158  fourierdlem34  43177  fourierdlem41  43184  fourierdlem46  43188  fourierdlem48  43190  fourierdlem49  43191  fourierdlem50  43192  fourierdlem54  43196  fourierdlem63  43205  fourierdlem64  43206  fourierdlem65  43207  fourierdlem79  43221  fourierdlem102  43244  fourierdlem103  43245  fourierdlem104  43246  fourierdlem114  43256  elaa2lem  43269  etransclem4  43274  etransclem7  43277  etransclem8  43278  etransclem17  43287  etransclem18  43288  etransclem20  43290  etransclem23  43293  etransclem27  43297  etransclem31  43301  etransclem32  43302  etransclem35  43305  etransclem41  43311  etransclem46  43316  etransclem48  43318  iundjiun  43493  caratheodorylem1  43559  2elfz2melfz  44271  elfzelfzlble  44274  el1fzopredsuc  44278  iccpartgtprec  44333  iccpartiltu  44335  iccpartgt  44340  iccpartnel  44351  fargshiftfo  44355  altgsumbc  45149  altgsumbcALT  45150  nn0sumshdiglemA  45426  nn0sumshdiglemB  45427