Theorem elfzelz 12342

Description: A member of a finite set of sequential integer 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 12338	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		eluzelz 11697	. 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ ℤ)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 1990  ‘cfv 5888  (class class class)co 6650  ℤcz 11377  ℤ_≥cuz 11687  ...cfz 12326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-1st 7168  df-2nd 7169  df-neg 10269  df-z 11378  df-uz 11688  df-fz 12327

This theorem is referenced by:  fzssz  12343  elfz1eq  12352  fzsplit2  12366  fzdisj  12368  elfznn  12370  ssfzunsnext  12386  fznatpl1  12395  fzrev2i  12405  fzrev3i  12407  fznuz  12422  fzrevral  12425  fzshftral  12428  fznn0sub2  12446  elfzmlbm  12449  difelfznle  12453  predfz  12464  fzosplit  12501  fz1fzo0m1  12515  sermono  12833  seqf1olem1  12840  seqf1olem2  12841  bcval2  13092  bcval4  13094  bccmpl  13096  bcp1nk  13104  bcval5  13105  bcpasc  13108  bccl2  13110  seqcoll  13248  seqcoll2  13249  swrdval2  13420  swrd0val  13421  addlenrevswrd  13437  swrd0fv  13439  ccatswrd  13456  swrdswrd  13460  swrdswrd0  13462  swrdccatin12lem2a  13485  swrdccatin12lem2b  13486  swrdccatin2  13487  swrdccatin12  13491  spllen  13505  splfv1  13506  cshwidxm  13554  cshwidxn  13555  lswcshw  13561  2cshwcshw  13571  cshwcshid  13573  cshwcsh2id  13574  seqshft  13825  sumrblem  14442  summolem2a  14446  fsum0diaglem  14508  mptfzshft  14510  fsumrev  14511  fsumshftm  14513  fsum0diag2  14515  binomlem  14561  binom11  14564  bcxmas  14567  arisum  14592  geo2sum  14604  mertenslem1  14616  prodfn0  14626  prodrblem  14659  prodmolem2a  14664  fprodntriv  14672  fprodser  14679  fprod1p  14698  fprodrev  14707  fallfacval3  14743  fallfacfwd  14767  0fallfac  14768  binomfallfaclem1  14770  binomfallfaclem2  14771  binomrisefac  14773  fallfacval4  14774  bpolycl  14783  bpolysum  14784  bpolydiflem  14785  fsumkthpow  14787  bpoly4  14790  fzm1ndvds  15044  pwp1fsum  15114  prmdvdsfz  15417  isprm7  15420  hashdvds  15480  phiprmpw  15481  prmdiveq  15491  prmdivdiv  15492  modprminv  15504  modprminveq  15505  modprm0  15510  4sqlem11  15659  4sqlem12  15660  vdwapun  15678  prmop1  15742  prmdvdsprmo  15746  prmdvdsprmop  15747  prmgaplem1  15753  prmgaplem2  15754  prmgaplcmlem1  15755  prmgaplcmlem2  15756  prmgapprmo  15766  cshwshashlem1  15802  cshwshashlem2  15803  dfod2  17981  efgredleme  18156  efgredlemc  18158  efgredlemb  18159  gsummptshft  18336  srgbinomlem3  18542  srgbinomlem4  18543  srgbinomlem  18544  chpscmatgsummon  20650  cayhamlem1  20671  iscmet3  23091  mbfi1fseqlem4  23485  itgz  23547  itgcl  23550  ibl0  23553  iblss  23571  iblss2  23572  itgss  23578  itgeqa  23580  iblconst  23584  iblabsr  23596  iblmulc2  23597  itgsplit  23602  dvfsumlem3  23791  plyeq0lem  23966  aalioulem1  24087  cxpeq  24498  birthdaylem2  24679  wilthlem1  24794  wilthlem2  24795  wilthlem3  24796  ftalem5  24803  basellem3  24809  basellem4  24810  dvdsppwf1o  24912  dvdsflf1o  24913  musum  24917  ppiub  24929  chtublem  24936  mersenne  24952  bposlem1  25009  lgsval2lem  25032  lgsdilem2  25058  lgsqrlem2  25072  lgsqrlem4  25074  gausslemma2dlem1a  25090  gausslemma2dlem1  25091  gausslemma2dlem3  25093  gausslemma2dlem4  25094  gausslemma2dlem5a  25095  gausslemma2dlem5  25096  gausslemma2dlem6  25097  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  2lgslem1a1  25114  2lgslem1a  25116  2lgslem1b  25117  rpvmasumlem  25176  dchrisumlem1  25178  dchrisumlem2  25179  dchrmusum2  25183  dchrvmasumlem1  25184  dchrvmasum2lem  25185  dchrvmasum2if  25186  dchrvmasumlem3  25188  dchrvmasumiflem1  25190  dchrvmasumiflem2  25191  dchrisum0flblem1  25197  rpvmasum2  25201  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0lem3  25208  dchrmusumlem  25211  dchrvmasumlem  25212  logdivbnd  25245  pntpbnd1  25275  pntlemh  25288  pntlemj  25292  pntlemf  25294  ostth2lem2  25323  axlowdimlem13  25834  axlowdimlem14  25835  axlowdimlem16  25837  crctcshlem4  26712  crctcshwlkn0  26713  clwwnisshclwwsn  26930  erclwwlkseqlen  26933  eleclclwwlksnlem2  26939  erclwwlksneqlen  26945  clwlksfclwwlk  26962  fzsplit3  29553  bcm1n  29554  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemodife  30559  ballotlemimin  30567  ballotlemsgt1  30572  ballotlemsel1i  30574  ballotlemsf1o  30575  ballotlemsi  30576  ballotlemsima  30577  ballotlemfg  30587  ballotlemfrc  30588  ballotlemfrceq  30590  ballotlemfrcn0  30591  ballotlemirc  30593  ballotlem1ri  30596  erdszelem8  31180  erdszelem9  31181  cvmliftlem7  31273  supfz  31613  inffz  31614  inffzOLD  31615  bcprod  31624  fwddifnp1  32272  poimirlem1  33410  poimirlem2  33411  poimirlem7  33416  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem23  33432  poimirlem24  33433  poimirlem27  33436  poimirlem28  33437  poimirlem31  33440  poimirlem32  33441  mblfinlem2  33447  iblmulc2nc  33475  fdc  33541  irrapxlem1  37386  irrapxlem2  37387  irrapxlem3  37388  pellexlem5  37397  acongrep  37547  fzmaxdif  37548  acongeq  37550  jm2.22  37562  jm2.23  37563  jm2.26lem3  37568  jm2.26  37569  jm2.27dlem2  37577  hashnzfz  38519  monoords  39511  elfzelzd  39530  fmul01lt1lem1  39816  fmul01lt1lem2  39817  sumnnodd  39862  limsupubuzlem  39944  dvnmul  40158  dvnprodlem2  40162  iblsplit  40182  iblspltprt  40189  itgspltprt  40195  stoweidlem3  40220  stoweidlem11  40228  stoweidlem20  40237  stoweidlem26  40243  stoweidlem34  40251  stoweidlem59  40276  stirlinglem10  40300  dirkertrigeqlem1  40315  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkeritg  40319  fourierdlem11  40335  fourierdlem12  40336  fourierdlem15  40339  fourierdlem34  40358  fourierdlem41  40365  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem54  40377  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem79  40402  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem114  40437  elaa2lem  40450  etransclem4  40455  etransclem7  40458  etransclem8  40459  etransclem17  40468  etransclem18  40469  etransclem20  40471  etransclem23  40474  etransclem27  40478  etransclem31  40482  etransclem32  40483  etransclem35  40486  etransclem41  40492  etransclem46  40497  etransclem48  40499  iundjiun  40677  caratheodorylem1  40740  2elfz2melfz  41328  elfzelfzlble  41331  el1fzopredsuc  41335  iccpartgtprec  41356  iccpartiltu  41358  iccpartgt  41363  iccpartnel  41374  fargshiftfo  41378  addlenrevpfx  41397  ccatpfx  41409  pfxccatin12lem1  41423  pfxccatin12lem2  41424  pfxccatin12  41425  altgsumbc  42130  altgsumbcALT  42131  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414