Theorem elfzelz 13550

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

Syntax hints:   → wi 4   ∈ wcel 2098  ‘cfv 6553  (class class class)co 7423  ℤcz 12605  ℤ_≥cuz 12869  ...cfz 13533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pr 5432  ax-un 7745  ax-cnex 11210  ax-resscn 11211

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5579  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-fv 6561  df-ov 7426  df-oprab 7427  df-mpo 7428  df-1st 8002  df-2nd 8003  df-neg 11493  df-z 12606  df-uz 12870  df-fz 13534

This theorem is referenced by:  elfzelzd  13551  fzssz  13552  elfz1eq  13561  fzsplit2  13575  fzdisj  13577  elfznn  13579  ssfzunsnext  13595  fznatpl1  13604  fzrev2i  13615  fzrev3i  13617  fznuz  13632  fzrevral  13635  fzshftral  13638  fznn0sub2  13657  elfzmlbm  13660  difelfznle  13664  predfz  13675  fzosplit  13714  sermono  14049  seqf1olem1  14056  seqf1olem2  14057  bcval2  14317  bcval4  14319  bccmpl  14321  bcp1nk  14329  bcval5  14330  bcpasc  14333  bccl2  14335  seqcoll2  14479  swrdval2  14649  swrdwrdsymb  14665  addlenrevpfx  14693  ccatpfx  14704  swrdswrd  14708  swrdpfx  14710  pfxccatin12lem2a  14730  pfxccatin12lem1  14731  swrdccatin2  14732  pfxccatin12lem2  14734  pfxccatin12  14736  spllen  14757  cshwidxm  14811  cshwidxn  14812  lswcshw  14818  2cshwcshw  14829  cshwcshid  14831  cshwcsh2id  14832  swrds2m  14945  seqshft  15085  sumrblem  15710  summolem2a  15714  fsum0diaglem  15775  mptfzshft  15777  fsumshftm  15780  fsum0diag2  15782  binomlem  15828  binom11  15831  bcxmas  15834  arisum  15859  geo2sum  15872  mertenslem1  15883  prodfn0  15893  prodrblem  15926  prodmolem2a  15931  fprodntriv  15939  fprodser  15946  fprodrev  15974  fallfacval3  16009  fallfacfwd  16033  0fallfac  16034  binomfallfaclem1  16036  binomfallfaclem2  16037  binomrisefac  16039  fallfacval4  16040  bpolycl  16049  bpolysum  16050  bpolydiflem  16051  fsumkthpow  16053  bpoly4  16056  fzm1ndvds  16319  pwp1fsum  16388  prmdvdsfz  16701  isprm7  16704  prmdvdsbc  16723  hashdvds  16772  phiprmpw  16773  prmdiveq  16783  modprminv  16796  modprminveq  16797  modprm0  16802  4sqlem11  16952  vdwapun  16971  prmop1  17035  prmdvdsprmo  17039  prmdvdsprmop  17040  prmgaplem1  17046  prmgaplem2  17047  prmgaplcmlem1  17048  prmgaplcmlem2  17049  prmgapprmo  17059  cshwshashlem1  17093  cshwshashlem2  17094  dfod2  19557  gsummptshft  19929  srgbinomlem3  20206  srgbinomlem4  20207  srgbinomlem  20208  freshmansdream  21564  chpscmatgsummon  22830  cayhamlem1  22851  iscmet3  25304  mbfi1fseqlem4  25731  itgz  25793  itgcl  25796  ibl0  25799  iblss  25817  iblss2  25818  itgss  25824  itgeqa  25826  iblconst  25830  iblabsr  25842  iblmulc2  25843  itgsplit  25848  dvfsumlem3  26046  plyeq0lem  26229  aalioulem1  26352  cxpeq  26777  birthdaylem2  26972  wilthlem1  27088  wilthlem3  27090  ftalem5  27097  basellem3  27103  basellem4  27104  dvdsppwf1o  27206  dvdsflf1o  27207  musum  27211  ppiub  27225  chtublem  27232  mersenne  27248  bposlem1  27305  lgsval2lem  27328  lgsdilem2  27354  lgsqrlem2  27368  gausslemma2dlem1a  27386  gausslemma2dlem1  27387  gausslemma2dlem3  27389  gausslemma2dlem4  27390  gausslemma2dlem5a  27391  gausslemma2dlem5  27392  gausslemma2dlem6  27393  lgseisenlem1  27396  lgseisenlem2  27397  lgseisenlem3  27398  lgsquadlem1  27401  lgsquadlem2  27402  lgsquadlem3  27403  2lgslem1a1  27410  2lgslem1a  27412  2lgslem1b  27413  rpvmasumlem  27508  dchrisumlem1  27510  dchrisumlem2  27511  dchrmusum2  27515  dchrvmasumlem1  27516  dchrvmasum2lem  27517  dchrvmasum2if  27518  dchrvmasumlem3  27520  dchrvmasumiflem1  27522  dchrvmasumiflem2  27523  dchrisum0flblem1  27529  rpvmasum2  27533  dchrisum0lem1b  27536  dchrisum0lem1  27537  dchrisum0lem2a  27538  dchrisum0lem2  27539  dchrisum0lem3  27540  dchrmusumlem  27543  dchrvmasumlem  27544  logdivbnd  27577  pntpbnd1  27607  pntlemh  27620  pntlemf  27626  ostth2lem2  27655  axlowdimlem13  28880  axlowdimlem14  28881  axlowdimlem16  28883  crctcshlem4  29746  crctcshwlkn0  29747  erclwwlkeqlen  29944  clwwnisshclwwsn  29984  eleclclwwlknlem2  29986  erclwwlkneqlen  29993  fzm1ne1  32680  fzsplit3  32685  bcm1n  32686  ballotlemfc0  34282  ballotlemfcc  34283  ballotlemodife  34287  ballotlemimin  34295  ballotlemsgt1  34300  ballotlemsel1i  34302  ballotlemsf1o  34303  ballotlemsi  34304  ballotlemsima  34305  ballotlemfg  34315  ballotlemfrc  34316  ballotlemfrcn0  34319  revpfxsfxrev  34895  swrdrevpfx  34896  pfxwlk  34903  swrdwlk  34906  erdszelem8  34978  erdszelem9  34979  cvmliftlem7  35071  supfz  35499  inffz  35500  bcprod  35508  fwddifnp1  35937  poimirlem1  37270  poimirlem14  37283  poimirlem15  37284  poimirlem16  37285  poimirlem17  37286  poimirlem19  37288  poimirlem20  37289  poimirlem23  37292  poimirlem24  37293  poimirlem27  37296  poimirlem31  37300  poimirlem32  37301  mblfinlem2  37307  iblmulc2nc  37334  fdc  37394  lcmineqlem1  41676  lcmineqlem6  41681  lcmineqlem17  41692  aks4d1p1p1  41710  aks6d1c1  41762  hashscontpow  41768  aks6d1c5lem0  41781  aks6d1c5lem3  41783  aks6d1c5  41785  sticksstones6  41797  sticksstones7  41798  sticksstones10  41801  sticksstones12a  41803  sticksstones12  41804  aks6d1c6lem1  41816  bcled  41824  bcle2d  41825  metakunt15  41848  metakunt16  41849  metakunt19  41852  metakunt25  41858  metakunt33  41866  sumcubes  42054  irrapxlem1  42416  irrapxlem2  42417  irrapxlem3  42418  pellexlem5  42427  acongrep  42575  acongeq  42578  jm2.22  42590  jm2.23  42591  jm2.26lem3  42596  jm2.27dlem2  42605  hashnzfz  43931  monoords  44849  fmul01lt1lem1  45142  fmul01lt1lem2  45143  sumnnodd  45188  limsupubuzlem  45270  dvnmul  45501  dvnprodlem2  45505  iblsplit  45524  iblspltprt  45531  itgspltprt  45537  stoweidlem3  45561  stoweidlem11  45569  stoweidlem20  45578  stoweidlem26  45584  stoweidlem34  45592  stoweidlem59  45617  stirlinglem10  45641  dirkertrigeqlem1  45656  dirkertrigeqlem2  45657  dirkertrigeqlem3  45658  dirkertrigeq  45659  dirkeritg  45660  fourierdlem11  45676  fourierdlem12  45677  fourierdlem15  45680  fourierdlem34  45699  fourierdlem41  45706  fourierdlem46  45710  fourierdlem48  45712  fourierdlem49  45713  fourierdlem50  45714  fourierdlem54  45718  fourierdlem63  45727  fourierdlem64  45728  fourierdlem65  45729  fourierdlem79  45743  fourierdlem102  45766  fourierdlem103  45767  fourierdlem104  45768  fourierdlem114  45778  elaa2lem  45791  etransclem4  45796  etransclem7  45799  etransclem8  45800  etransclem17  45809  etransclem18  45810  etransclem20  45812  etransclem23  45815  etransclem27  45819  etransclem31  45823  etransclem32  45824  etransclem35  45827  etransclem41  45833  etransclem46  45838  etransclem48  45840  iundjiun  46018  caratheodorylem1  46084  2elfz2melfz  46868  elfzelfzlble  46871  el1fzopredsuc  46875  iccpartiltu  46931  iccpartgt  46936  iccpartnel  46947  fargshiftfo  46951  altgsumbc  47668  altgsumbcALT  47669  nn0sumshdiglemA  47944  nn0sumshdiglemB  47945