Theorem elfzelz 13498

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

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6541  (class class class)co 7406  ℤcz 12555  ℤ_≥cuz 12819  ...cfz 13481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-1st 7972  df-2nd 7973  df-neg 11444  df-z 12556  df-uz 12820  df-fz 13482

This theorem is referenced by:  elfzelzd  13499  fzssz  13500  elfz1eq  13509  fzsplit2  13523  fzdisj  13525  elfznn  13527  ssfzunsnext  13543  fznatpl1  13552  fzrev2i  13563  fzrev3i  13565  fznuz  13580  fzrevral  13583  fzshftral  13586  fznn0sub2  13605  elfzmlbm  13608  difelfznle  13612  predfz  13623  fzosplit  13662  sermono  13997  seqf1olem1  14004  seqf1olem2  14005  bcval2  14262  bcval4  14264  bccmpl  14266  bcp1nk  14274  bcval5  14275  bcpasc  14278  bccl2  14280  seqcoll2  14423  swrdval2  14593  swrdwrdsymb  14609  addlenrevpfx  14637  ccatpfx  14648  swrdswrd  14652  swrdpfx  14654  pfxccatin12lem2a  14674  pfxccatin12lem1  14675  swrdccatin2  14676  pfxccatin12lem2  14678  pfxccatin12  14680  spllen  14701  cshwidxm  14755  cshwidxn  14756  lswcshw  14762  2cshwcshw  14773  cshwcshid  14775  cshwcsh2id  14776  swrds2m  14889  seqshft  15029  sumrblem  15654  summolem2a  15658  fsum0diaglem  15719  mptfzshft  15721  fsumshftm  15724  fsum0diag2  15726  binomlem  15772  binom11  15775  bcxmas  15778  arisum  15803  geo2sum  15816  mertenslem1  15827  prodfn0  15837  prodrblem  15870  prodmolem2a  15875  fprodntriv  15883  fprodser  15890  fprodrev  15918  fallfacval3  15953  fallfacfwd  15977  0fallfac  15978  binomfallfaclem1  15980  binomfallfaclem2  15981  binomrisefac  15983  fallfacval4  15984  bpolycl  15993  bpolysum  15994  bpolydiflem  15995  fsumkthpow  15997  bpoly4  16000  fzm1ndvds  16262  pwp1fsum  16331  prmdvdsfz  16639  isprm7  16642  hashdvds  16705  phiprmpw  16706  prmdiveq  16716  modprminv  16729  modprminveq  16730  modprm0  16735  4sqlem11  16885  vdwapun  16904  prmop1  16968  prmdvdsprmo  16972  prmdvdsprmop  16973  prmgaplem1  16979  prmgaplem2  16980  prmgaplcmlem1  16981  prmgaplcmlem2  16982  prmgapprmo  16992  cshwshashlem1  17026  cshwshashlem2  17027  dfod2  19427  gsummptshft  19799  srgbinomlem3  20045  srgbinomlem4  20046  srgbinomlem  20047  chpscmatgsummon  22339  cayhamlem1  22360  iscmet3  24802  mbfi1fseqlem4  25228  itgz  25290  itgcl  25293  ibl0  25296  iblss  25314  iblss2  25315  itgss  25321  itgeqa  25323  iblconst  25327  iblabsr  25339  iblmulc2  25340  itgsplit  25345  dvfsumlem3  25537  plyeq0lem  25716  aalioulem1  25837  cxpeq  26255  birthdaylem2  26447  wilthlem1  26562  wilthlem3  26564  ftalem5  26571  basellem3  26577  basellem4  26578  dvdsppwf1o  26680  dvdsflf1o  26681  musum  26685  ppiub  26697  chtublem  26704  mersenne  26720  bposlem1  26777  lgsval2lem  26800  lgsdilem2  26826  lgsqrlem2  26840  gausslemma2dlem1a  26858  gausslemma2dlem1  26859  gausslemma2dlem3  26861  gausslemma2dlem4  26862  gausslemma2dlem5a  26863  gausslemma2dlem5  26864  gausslemma2dlem6  26865  lgseisenlem1  26868  lgseisenlem2  26869  lgseisenlem3  26870  lgsquadlem1  26873  lgsquadlem2  26874  lgsquadlem3  26875  2lgslem1a1  26882  2lgslem1a  26884  2lgslem1b  26885  rpvmasumlem  26980  dchrisumlem1  26982  dchrisumlem2  26983  dchrmusum2  26987  dchrvmasumlem1  26988  dchrvmasum2lem  26989  dchrvmasum2if  26990  dchrvmasumlem3  26992  dchrvmasumiflem1  26994  dchrvmasumiflem2  26995  dchrisum0flblem1  27001  rpvmasum2  27005  dchrisum0lem1b  27008  dchrisum0lem1  27009  dchrisum0lem2a  27010  dchrisum0lem2  27011  dchrisum0lem3  27012  dchrmusumlem  27015  dchrvmasumlem  27016  logdivbnd  27049  pntpbnd1  27079  pntlemh  27092  pntlemf  27098  ostth2lem2  27127  axlowdimlem13  28202  axlowdimlem14  28203  axlowdimlem16  28205  crctcshlem4  29064  crctcshwlkn0  29065  erclwwlkeqlen  29262  clwwnisshclwwsn  29302  eleclclwwlknlem2  29304  erclwwlkneqlen  29311  fzm1ne1  31988  fzsplit3  31993  bcm1n  31994  prmdvdsbc  32010  freshmansdream  32370  ballotlemfc0  33480  ballotlemfcc  33481  ballotlemodife  33485  ballotlemimin  33493  ballotlemsgt1  33498  ballotlemsel1i  33500  ballotlemsf1o  33501  ballotlemsi  33502  ballotlemsima  33503  ballotlemfg  33513  ballotlemfrc  33514  ballotlemfrcn0  33517  revpfxsfxrev  34095  swrdrevpfx  34096  pfxwlk  34103  swrdwlk  34106  erdszelem8  34178  erdszelem9  34179  cvmliftlem7  34271  supfz  34687  inffz  34688  bcprod  34697  fwddifnp1  35126  poimirlem1  36478  poimirlem14  36491  poimirlem15  36492  poimirlem16  36493  poimirlem17  36494  poimirlem19  36496  poimirlem20  36497  poimirlem23  36500  poimirlem24  36501  poimirlem27  36504  poimirlem31  36508  poimirlem32  36509  mblfinlem2  36515  iblmulc2nc  36542  fdc  36602  lcmineqlem1  40883  lcmineqlem6  40888  lcmineqlem17  40899  aks4d1p1p1  40917  sticksstones6  40956  sticksstones7  40957  sticksstones10  40960  sticksstones12a  40962  sticksstones12  40963  metakunt15  40988  metakunt16  40989  metakunt19  40992  metakunt25  40998  metakunt33  41006  sumcubes  41207  irrapxlem1  41546  irrapxlem2  41547  irrapxlem3  41548  pellexlem5  41557  acongrep  41705  acongeq  41708  jm2.22  41720  jm2.23  41721  jm2.26lem3  41726  jm2.27dlem2  41735  hashnzfz  43065  monoords  43994  fmul01lt1lem1  44287  fmul01lt1lem2  44288  sumnnodd  44333  limsupubuzlem  44415  dvnmul  44646  dvnprodlem2  44650  iblsplit  44669  iblspltprt  44676  itgspltprt  44682  stoweidlem3  44706  stoweidlem11  44714  stoweidlem20  44723  stoweidlem26  44729  stoweidlem34  44737  stoweidlem59  44762  stirlinglem10  44786  dirkertrigeqlem1  44801  dirkertrigeqlem2  44802  dirkertrigeqlem3  44803  dirkertrigeq  44804  dirkeritg  44805  fourierdlem11  44821  fourierdlem12  44822  fourierdlem15  44825  fourierdlem34  44844  fourierdlem41  44851  fourierdlem46  44855  fourierdlem48  44857  fourierdlem49  44858  fourierdlem50  44859  fourierdlem54  44863  fourierdlem63  44872  fourierdlem64  44873  fourierdlem65  44874  fourierdlem79  44888  fourierdlem102  44911  fourierdlem103  44912  fourierdlem104  44913  fourierdlem114  44923  elaa2lem  44936  etransclem4  44941  etransclem7  44944  etransclem8  44945  etransclem17  44954  etransclem18  44955  etransclem20  44957  etransclem23  44960  etransclem27  44964  etransclem31  44968  etransclem32  44969  etransclem35  44972  etransclem41  44978  etransclem46  44983  etransclem48  44985  iundjiun  45163  caratheodorylem1  45229  2elfz2melfz  46013  elfzelfzlble  46016  el1fzopredsuc  46020  iccpartiltu  46077  iccpartgt  46082  iccpartnel  46093  fargshiftfo  46097  altgsumbc  46982  altgsumbcALT  46983  nn0sumshdiglemA  47259  nn0sumshdiglemB  47260