Theorem elfzelz 13570

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ‘cfv 6543  (class class class)co 7423  ℤcz 12609  ℤ_≥cuz 12880  ...cfz 13553

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 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-1st 7995  df-2nd 7996  df-neg 11462  df-z 12610  df-uz 12881  df-fz 13554

This theorem is used by:  elfzelzd  13571  fzssz  13572  elfz1eq  13581  fzsplit2  13596  fzdisj  13598  elfznn  13600  ssfzunsnext  13616  fznatpl1  13625  fzrev2i  13636  fzrev3i  13638  fznuz  13656  fzrevral  13659  fzshftral  13662  fznn0sub2  13682  elfzmlbm  13685  difelfznle  13689  predfz  13700  fzosplit  13740  sermono  14090  seqf1olem1  14097  seqf1olem2  14098  bcval2  14361  bcval4  14363  bccmpl  14365  bcp1nk  14373  bcval5  14374  bcpasc  14377  bccl2  14379  seqcoll2  14522  swrdval2  14706  swrdwrdsymb  14724  ccatpfx  14762  swrdswrd  14766  swrdpfx  14768  pfxccatin12lem2a  14788  pfxccatin12lem1  14789  swrdccatin2  14790  pfxccatin12lem2  14792  pfxccatin12  14794  spllen  14815  revpfxsfxrev  14829  swrdrevpfx  14830  cshwidxm  14871  cshwidxn  14872  lswcshw  14878  2cshwcshw  14888  cshwcshid  14890  cshwcsh2id  14891  swrds2m  15004  seqshft  15148  sumrblem  15788  summolem2a  15792  fsum0diaglem  15853  mptfzshft  15855  fsumshftm  15858  fsum0diag2  15860  binomlem  15909  binom11  15912  bcxmas  15915  arisum  15940  geo2sum  15953  mertenslem1  15964  prodfn0  15974  prodrblem  16009  prodmolem2a  16014  fprodntriv  16022  fprodser  16029  fprodrev  16057  fallfacval3  16092  fallfacfwd  16115  0fallfac  16116  binomfallfaclem1  16118  binomfallfaclem2  16119  binomrisefac  16121  fallfacval4  16122  bpolycl  16131  bpolysum  16132  bpolydiflem  16133  fsumkthpow  16135  bpoly4  16138  fzm1ndvds  16405  pwp1fsum  16474  prmdvdsfz  16789  isprm7  16792  prmdvdsbc  16810  hashdvds  16859  phiprmpw  16860  prmdiveq  16870  modprminv  16884  modprminveq  16885  modprm0  16890  4sqlem11  17040  vdwapun  17059  prmop1  17123  prmdvdsprmo  17127  prmdvdsprmop  17128  prmgaplem1  17134  prmgaplem2  17135  prmgaplcmlem1  17136  prmgaplcmlem2  17137  prmgapprmo  17147  cshwshashlem1  17180  cshwshashlem2  17181  dfod2  19665  gsummptshft  20037  srgbinomlem3  20341  srgbinomlem4  20342  srgbinomlem  20343  freshmansdream  21761  chpscmatgsummon  23039  cayhamlem1  23060  iscmet3  25489  mbfi1fseqlem4  25914  itgz  25977  itgcl  25980  ibl0  25983  iblss  26001  iblss2  26002  itgss  26008  itgeqa  26010  iblconst  26014  iblabsr  26026  iblmulc2  26027  itgsplit  26032  dvfsumlem3  26224  plyeq0lem  26404  aalioulem1  26532  cxpeq  26959  birthdaylem2  27154  wilthlem1  27269  wilthlem3  27271  ftalem5  27278  basellem3  27284  basellem4  27285  dvdsppwf1o  27387  dvdsflf1o  27388  musum  27392  ppiub  27405  chtublem  27412  mersenne  27428  bposlem1  27485  lgsval2lem  27508  lgsdilem2  27534  lgsqrlem2  27548  gausslemma2dlem1a  27566  gausslemma2dlem1  27567  gausslemma2dlem3  27569  gausslemma2dlem4  27570  gausslemma2dlem5a  27571  gausslemma2dlem5  27572  gausslemma2dlem6  27573  lgseisenlem1  27576  lgseisenlem2  27577  lgseisenlem3  27578  lgsquadlem1  27581  lgsquadlem2  27582  lgsquadlem3  27583  2lgslem1a1  27590  2lgslem1a  27592  2lgslem1b  27593  rpvmasumlem  27688  dchrisumlem1  27690  dchrisumlem2  27691  dchrmusum2  27695  dchrvmasumlem1  27696  dchrvmasum2lem  27697  dchrvmasum2if  27698  dchrvmasumlem3  27700  dchrvmasumiflem1  27702  dchrvmasumiflem2  27703  dchrisum0flblem1  27709  rpvmasum2  27713  dchrisum0lem1b  27716  dchrisum0lem1  27717  dchrisum0lem2a  27718  dchrisum0lem2  27719  dchrisum0lem3  27720  dchrmusumlem  27723  dchrvmasumlem  27724  logdivbnd  27757  pntpbnd1  27787  pntlemh  27800  pntlemf  27806  ostth2lem2  27835  axlowdimlem13  29341  axlowdimlem14  29342  axlowdimlem16  29344  crctcshlem4  30206  crctcshwlkn0  30207  erclwwlkeqlen  30407  clwwnisshclwwsn  30447  eleclclwwlknlem2  30449  erclwwlkneqlen  30456  fzm1ne1  33170  fzsplit3  33175  bcm1n  33177  ballotlemfc0  34914  ballotlemfcc  34915  ballotlemodife  34919  ballotlemimin  34927  ballotlemsgt1  34932  ballotlemsel1i  34934  ballotlemsf1o  34935  ballotlemsi  34936  ballotlemsima  34937  ballotlemfg  34947  ballotlemfrc  34948  ballotlemfrcn0  34951  pfxwlk  35636  swrdwlk  35639  erdszelem8  35710  erdszelem9  35711  cvmliftlem7  35803  supfz  36241  inffz  36242  bcprod  36250  fwddifnp1  36677  poimirlem1  38312  poimirlem14  38325  poimirlem15  38326  poimirlem16  38327  poimirlem17  38328  poimirlem19  38330  poimirlem20  38331  poimirlem23  38334  poimirlem24  38335  poimirlem27  38338  poimirlem31  38342  poimirlem32  38343  mblfinlem2  38349  iblmulc2nc  38376  fdc  38436  lcmineqlem1  42836  lcmineqlem6  42841  lcmineqlem17  42852  aks4d1p1p1  42870  aks6d1c1  42923  hashscontpow  42929  aks6d1c5lem0  42942  aks6d1c5lem3  42944  aks6d1c5  42946  sticksstones6  42958  sticksstones7  42959  sticksstones10  42962  sticksstones12a  42964  sticksstones12  42965  aks6d1c6lem1  42977  bcled  42985  bcle2d  42986  aks5lem5a  42998  grpods  43001  unitscyglem2  43003  unitscyglem4  43005  sumcubes  43114  irrapxlem1  43589  irrapxlem2  43590  irrapxlem3  43591  pellexlem5  43600  acongrep  43747  acongeq  43750  jm2.22  43762  jm2.23  43763  jm2.26lem3  43768  jm2.27dlem2  43777  hashnzfz  45070  monoords  46056  fmul01lt1lem1  46340  fmul01lt1lem2  46341  sumnnodd  46386  limsupubuzlem  46466  dvnmul  46697  dvnprodlem1  46700  dvnprodlem2  46701  iblsplit  46720  iblspltprt  46727  itgspltprt  46733  stoweidlem3  46757  stoweidlem11  46765  stoweidlem20  46774  stoweidlem26  46780  stoweidlem34  46788  stoweidlem59  46813  stirlinglem10  46837  dirkertrigeqlem1  46852  dirkertrigeqlem2  46853  dirkertrigeqlem3  46854  dirkertrigeq  46855  dirkeritg  46856  fourierdlem11  46872  fourierdlem12  46873  fourierdlem15  46876  fourierdlem34  46895  fourierdlem41  46902  fourierdlem46  46906  fourierdlem48  46908  fourierdlem49  46909  fourierdlem50  46910  fourierdlem54  46914  fourierdlem63  46923  fourierdlem64  46924  fourierdlem65  46925  fourierdlem79  46939  fourierdlem102  46962  fourierdlem103  46963  fourierdlem104  46964  fourierdlem114  46974  elaa2lem  46987  etransclem4  46992  etransclem7  46995  etransclem8  46996  etransclem17  47005  etransclem18  47006  etransclem20  47008  etransclem23  47011  etransclem27  47015  etransclem31  47019  etransclem32  47020  etransclem35  47023  etransclem41  47029  etransclem46  47034  etransclem48  47036  iundjiun  47214  caratheodorylem1  47280  2elfz2melfz  48095  elfzelfzlble  48098  el1fzopredsuc  48103  iccpartiltu  48211  iccpartgt  48216  iccpartnel  48227  fargshiftfo  48231  altgsumbc  49172  altgsumbcALT  49173  nn0sumshdiglemA  49439  nn0sumshdiglemB  49440