Theorem elfzelz 13578

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6533  (class class class)co 7413  ℤcz 12615  ℤ_≥cuz 12887  ...cfz 13561

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736  ax-cnex 11180  ax-resscn 11181

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7416  df-oprab 7417  df-mpo 7418  df-1st 7986  df-2nd 7987  df-neg 11468  df-z 12616  df-uz 12888  df-fz 13562

This theorem is used by:  elfzelzd  13579  fzssz  13580  elfz1eq  13589  fzsplit2  13604  fzdisj  13606  elfznn  13608  ssfzunsnext  13624  fznatpl1  13633  fzrev2i  13644  fzrev3i  13646  fznuz  13664  fzrevral  13667  fzshftral  13670  fznn0sub2  13690  elfzmlbm  13693  difelfznle  13697  predfz  13708  fzosplit  13748  sermono  14098  seqf1olem1  14105  seqf1olem2  14106  bcval2  14369  bcval4  14371  bccmpl  14373  bcp1nk  14381  bcval5  14382  bcpasc  14385  bccl2  14387  seqcoll2  14530  swrdval2  14714  swrdwrdsymb  14732  ccatpfx  14770  swrdswrd  14774  swrdpfx  14776  pfxccatin12lem2a  14796  pfxccatin12lem1  14797  swrdccatin2  14798  pfxccatin12lem2  14800  pfxccatin12  14802  spllen  14823  revpfxsfxrev  14837  swrdrevpfx  14838  cshwidxm  14879  cshwidxn  14880  lswcshw  14886  2cshwcshw  14896  cshwcshid  14898  cshwcsh2id  14899  swrds2m  15012  seqshft  15158  sumrblem  15797  summolem2a  15801  fsum0diaglem  15862  mptfzshft  15864  fsumshftm  15867  fsum0diag2  15869  binomlem  15918  binom11  15921  bcxmas  15924  arisum  15949  geo2sum  15962  mertenslem1  15973  prodfn0  15983  prodrblem  16016  prodmolem2a  16021  fprodntriv  16029  fprodser  16036  fprodrev  16064  fallfacval3  16099  fallfacfwd  16122  0fallfac  16123  binomfallfaclem1  16125  binomfallfaclem2  16126  binomrisefac  16128  fallfacval4  16129  bpolycl  16138  bpolysum  16139  bpolydiflem  16140  fsumkthpow  16142  bpoly4  16145  fzm1ndvds  16412  pwp1fsum  16481  prmdvdsfz  16796  isprm7  16799  prmdvdsbc  16817  hashdvds  16866  phiprmpw  16867  prmdiveq  16877  modprminv  16891  modprminveq  16892  modprm0  16897  4sqlem11  17047  vdwapun  17066  prmop1  17130  prmdvdsprmo  17134  prmdvdsprmop  17135  prmgaplem1  17141  prmgaplem2  17142  prmgaplcmlem1  17143  prmgaplcmlem2  17144  prmgapprmo  17154  cshwshashlem1  17187  cshwshashlem2  17188  dfod2  19691  gsummptshft  20063  srgbinomlem3  20367  srgbinomlem4  20368  srgbinomlem  20369  freshmansdream  21787  chpscmatgsummon  23070  cayhamlem1  23091  iscmet3  25521  mbfi1fseqlem4  25946  itgz  26008  itgcl  26011  ibl0  26014  iblss  26032  iblss2  26033  itgss  26039  itgeqa  26041  iblconst  26045  iblabsr  26057  iblmulc2  26058  itgsplit  26063  dvfsumlem3  26255  plyeq0lem  26436  aalioulem1  26568  cxpeq  26994  birthdaylem2  27189  wilthlem1  27304  wilthlem3  27306  ftalem5  27313  basellem3  27319  basellem4  27320  dvdsppwf1o  27422  dvdsflf1o  27423  musum  27427  ppiub  27440  chtublem  27447  mersenne  27463  bposlem1  27520  lgsval2lem  27543  lgsdilem2  27569  lgsqrlem2  27583  gausslemma2dlem1a  27601  gausslemma2dlem1  27602  gausslemma2dlem3  27604  gausslemma2dlem4  27605  gausslemma2dlem5a  27606  gausslemma2dlem5  27607  gausslemma2dlem6  27608  lgseisenlem1  27611  lgseisenlem2  27612  lgseisenlem3  27613  lgsquadlem1  27616  lgsquadlem2  27617  lgsquadlem3  27618  2lgslem1a1  27625  2lgslem1a  27627  2lgslem1b  27628  rpvmasumlem  27723  dchrisumlem1  27725  dchrisumlem2  27726  dchrmusum2  27730  dchrvmasumlem1  27731  dchrvmasum2lem  27732  dchrvmasum2if  27733  dchrvmasumlem3  27735  dchrvmasumiflem1  27737  dchrvmasumiflem2  27738  dchrisum0flblem1  27744  rpvmasum2  27748  dchrisum0lem1b  27751  dchrisum0lem1  27752  dchrisum0lem2a  27753  dchrisum0lem2  27754  dchrisum0lem3  27755  dchrmusumlem  27758  dchrvmasumlem  27759  logdivbnd  27792  pntpbnd1  27822  pntlemh  27835  pntlemf  27841  ostth2lem2  27870  axlowdimlem13  29411  axlowdimlem14  29412  axlowdimlem16  29414  pfxwlk  30145  swrdwlk  30147  crctcshlem4  30288  crctcshwlkn0  30289  erclwwlkeqlen  30489  clwwnisshclwwsn  30529  eleclclwwlknlem2  30531  erclwwlkneqlen  30538  fzm1ne1  33259  fzsplit3  33264  bcm1n  33266  ballotlemfc0  35004  ballotlemfcc  35005  ballotlemodife  35009  ballotlemimin  35017  ballotlemsgt1  35022  ballotlemsel1i  35024  ballotlemsf1o  35025  ballotlemsi  35026  ballotlemsima  35027  ballotlemfg  35037  ballotlemfrc  35038  ballotlemfrcn0  35041  erdszelem8  35777  erdszelem9  35778  cvmliftlem7  35870  supfz  36308  inffz  36309  bcprod  36317  fwddifnp1  36745  poimirlem1  38370  poimirlem14  38383  poimirlem15  38384  poimirlem16  38385  poimirlem17  38386  poimirlem19  38388  poimirlem20  38389  poimirlem23  38392  poimirlem24  38393  poimirlem27  38396  poimirlem31  38400  poimirlem32  38401  mblfinlem2  38407  iblmulc2nc  38434  fdc  38495  lcmineqlem1  42895  lcmineqlem6  42900  lcmineqlem17  42911  aks4d1p1p1  42929  aks6d1c1  42982  hashscontpow  42988  aks6d1c5lem0  43001  aks6d1c5lem3  43003  aks6d1c5  43005  sticksstones6  43017  sticksstones7  43018  sticksstones10  43021  sticksstones12a  43023  sticksstones12  43024  aks6d1c6lem1  43036  bcled  43044  bcle2d  43045  aks5lem5a  43057  grpods  43060  unitscyglem2  43062  unitscyglem4  43064  sumcubes  43188  irrapxlem1  43663  irrapxlem2  43664  irrapxlem3  43665  pellexlem5  43674  acongrep  43821  acongeq  43824  jm2.22  43836  jm2.23  43837  jm2.26lem3  43842  jm2.27dlem2  43851  hashnzfz  45144  monoords  46130  fmul01lt1lem1  46414  fmul01lt1lem2  46415  sumnnodd  46460  limsupubuzlem  46540  dvnmul  46771  dvnprodlem1  46774  dvnprodlem2  46775  iblsplit  46794  iblspltprt  46801  itgspltprt  46807  stoweidlem3  46831  stoweidlem11  46839  stoweidlem20  46848  stoweidlem26  46854  stoweidlem34  46862  stoweidlem59  46887  stirlinglem10  46911  dirkertrigeqlem1  46926  dirkertrigeqlem2  46927  dirkertrigeqlem3  46928  dirkertrigeq  46929  dirkeritg  46930  fourierdlem11  46946  fourierdlem12  46947  fourierdlem15  46950  fourierdlem34  46969  fourierdlem41  46976  fourierdlem46  46980  fourierdlem48  46982  fourierdlem49  46983  fourierdlem50  46984  fourierdlem54  46988  fourierdlem63  46997  fourierdlem64  46998  fourierdlem65  46999  fourierdlem79  47013  fourierdlem102  47036  fourierdlem103  47037  fourierdlem104  47038  fourierdlem114  47048  elaa2lem  47061  etransclem4  47066  etransclem7  47069  etransclem8  47070  etransclem17  47079  etransclem18  47080  etransclem20  47082  etransclem23  47085  etransclem27  47089  etransclem31  47093  etransclem32  47094  etransclem35  47097  etransclem41  47103  etransclem46  47108  etransclem48  47110  iundjiun  47288  caratheodorylem1  47354  2elfz2melfz  48206  elfzelfzlble  48209  el1fzopredsuc  48214  iccpartiltu  48322  iccpartgt  48327  iccpartnel  48338  fargshiftfo  48342  altgsumbc  49282  altgsumbcALT  49283  nn0sumshdiglemA  49549  nn0sumshdiglemB  49550