MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfzelz Structured version   Visualization version   GIF version

Theorem elfzelz 13442
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
StepHypRef Expression
1 elfzuz 13438 . 2 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ𝑀))
2 eluzelz 12774 . 2 (𝐾 ∈ (ℤ𝑀) → 𝐾 ∈ ℤ)
31, 2syl 17 1 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cfv 6497  (class class class)co 7358  cz 12500  cuz 12764  ...cfz 13425
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 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673  ax-cnex 11108  ax-resscn 11109
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-neg 11389  df-z 12501  df-uz 12765  df-fz 13426
This theorem is referenced by:  elfzelzd  13443  fzssz  13444  elfz1eq  13453  fzsplit2  13467  fzdisj  13469  elfznn  13471  ssfzunsnext  13487  fznatpl1  13496  fzrev2i  13507  fzrev3i  13509  fznuz  13524  fzrevral  13527  fzshftral  13530  fznn0sub2  13549  elfzmlbm  13552  difelfznle  13556  predfz  13567  fzosplit  13606  sermono  13941  seqf1olem1  13948  seqf1olem2  13949  bcval2  14206  bcval4  14208  bccmpl  14210  bcp1nk  14218  bcval5  14219  bcpasc  14222  bccl2  14224  seqcoll2  14365  swrdval2  14535  swrdwrdsymb  14551  addlenrevpfx  14579  ccatpfx  14590  swrdswrd  14594  swrdpfx  14596  pfxccatin12lem2a  14616  pfxccatin12lem1  14617  swrdccatin2  14618  pfxccatin12lem2  14620  pfxccatin12  14622  spllen  14643  cshwidxm  14697  cshwidxn  14698  lswcshw  14704  2cshwcshw  14715  cshwcshid  14717  cshwcsh2id  14718  swrds2m  14831  seqshft  14971  sumrblem  15597  summolem2a  15601  fsum0diaglem  15662  mptfzshft  15664  fsumshftm  15667  fsum0diag2  15669  binomlem  15715  binom11  15718  bcxmas  15721  arisum  15746  geo2sum  15759  mertenslem1  15770  prodfn0  15780  prodrblem  15813  prodmolem2a  15818  fprodntriv  15826  fprodser  15833  fprodrev  15861  fallfacval3  15896  fallfacfwd  15920  0fallfac  15921  binomfallfaclem1  15923  binomfallfaclem2  15924  binomrisefac  15926  fallfacval4  15927  bpolycl  15936  bpolysum  15937  bpolydiflem  15938  fsumkthpow  15940  bpoly4  15943  fzm1ndvds  16205  pwp1fsum  16274  prmdvdsfz  16582  isprm7  16585  hashdvds  16648  phiprmpw  16649  prmdiveq  16659  modprminv  16672  modprminveq  16673  modprm0  16678  4sqlem11  16828  vdwapun  16847  prmop1  16911  prmdvdsprmo  16915  prmdvdsprmop  16916  prmgaplem1  16922  prmgaplem2  16923  prmgaplcmlem1  16924  prmgaplcmlem2  16925  prmgapprmo  16935  cshwshashlem1  16969  cshwshashlem2  16970  dfod2  19347  gsummptshft  19714  srgbinomlem3  19960  srgbinomlem4  19961  srgbinomlem  19962  chpscmatgsummon  22197  cayhamlem1  22218  iscmet3  24660  mbfi1fseqlem4  25086  itgz  25148  itgcl  25151  ibl0  25154  iblss  25172  iblss2  25173  itgss  25179  itgeqa  25181  iblconst  25185  iblabsr  25197  iblmulc2  25198  itgsplit  25203  dvfsumlem3  25395  plyeq0lem  25574  aalioulem1  25695  cxpeq  26113  birthdaylem2  26305  wilthlem1  26420  wilthlem3  26422  ftalem5  26429  basellem3  26435  basellem4  26436  dvdsppwf1o  26538  dvdsflf1o  26539  musum  26543  ppiub  26555  chtublem  26562  mersenne  26578  bposlem1  26635  lgsval2lem  26658  lgsdilem2  26684  lgsqrlem2  26698  gausslemma2dlem1a  26716  gausslemma2dlem1  26717  gausslemma2dlem3  26719  gausslemma2dlem4  26720  gausslemma2dlem5a  26721  gausslemma2dlem5  26722  gausslemma2dlem6  26723  lgseisenlem1  26726  lgseisenlem2  26727  lgseisenlem3  26728  lgsquadlem1  26731  lgsquadlem2  26732  lgsquadlem3  26733  2lgslem1a1  26740  2lgslem1a  26742  2lgslem1b  26743  rpvmasumlem  26838  dchrisumlem1  26840  dchrisumlem2  26841  dchrmusum2  26845  dchrvmasumlem1  26846  dchrvmasum2lem  26847  dchrvmasum2if  26848  dchrvmasumlem3  26850  dchrvmasumiflem1  26852  dchrvmasumiflem2  26853  dchrisum0flblem1  26859  rpvmasum2  26863  dchrisum0lem1b  26866  dchrisum0lem1  26867  dchrisum0lem2a  26868  dchrisum0lem2  26869  dchrisum0lem3  26870  dchrmusumlem  26873  dchrvmasumlem  26874  logdivbnd  26907  pntpbnd1  26937  pntlemh  26950  pntlemf  26956  ostth2lem2  26985  axlowdimlem13  27906  axlowdimlem14  27907  axlowdimlem16  27909  crctcshlem4  28768  crctcshwlkn0  28769  erclwwlkeqlen  28966  clwwnisshclwwsn  29006  eleclclwwlknlem2  29008  erclwwlkneqlen  29015  fzm1ne1  31695  fzsplit3  31700  bcm1n  31701  prmdvdsbc  31715  freshmansdream  32070  ballotlemfc0  33095  ballotlemfcc  33096  ballotlemodife  33100  ballotlemimin  33108  ballotlemsgt1  33113  ballotlemsel1i  33115  ballotlemsf1o  33116  ballotlemsi  33117  ballotlemsima  33118  ballotlemfg  33128  ballotlemfrc  33129  ballotlemfrcn0  33132  revpfxsfxrev  33712  swrdrevpfx  33713  pfxwlk  33720  swrdwlk  33723  erdszelem8  33795  erdszelem9  33796  cvmliftlem7  33888  supfz  34304  inffz  34305  bcprod  34314  fwddifnp1  34753  poimirlem1  36082  poimirlem14  36095  poimirlem15  36096  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem20  36101  poimirlem23  36104  poimirlem24  36105  poimirlem27  36108  poimirlem31  36112  poimirlem32  36113  mblfinlem2  36119  iblmulc2nc  36146  fdc  36207  lcmineqlem1  40489  lcmineqlem6  40494  lcmineqlem17  40505  aks4d1p1p1  40523  sticksstones6  40562  sticksstones7  40563  sticksstones10  40566  sticksstones12a  40568  sticksstones12  40569  metakunt15  40594  metakunt16  40595  metakunt19  40598  metakunt25  40604  metakunt33  40612  irrapxlem1  41148  irrapxlem2  41149  irrapxlem3  41150  pellexlem5  41159  acongrep  41307  acongeq  41310  jm2.22  41322  jm2.23  41323  jm2.26lem3  41328  jm2.27dlem2  41337  hashnzfz  42607  monoords  43538  fmul01lt1lem1  43832  fmul01lt1lem2  43833  sumnnodd  43878  limsupubuzlem  43960  dvnmul  44191  dvnprodlem2  44195  iblsplit  44214  iblspltprt  44221  itgspltprt  44227  stoweidlem3  44251  stoweidlem11  44259  stoweidlem20  44268  stoweidlem26  44274  stoweidlem34  44282  stoweidlem59  44307  stirlinglem10  44331  dirkertrigeqlem1  44346  dirkertrigeqlem2  44347  dirkertrigeqlem3  44348  dirkertrigeq  44349  dirkeritg  44350  fourierdlem11  44366  fourierdlem12  44367  fourierdlem15  44370  fourierdlem34  44389  fourierdlem41  44396  fourierdlem46  44400  fourierdlem48  44402  fourierdlem49  44403  fourierdlem50  44404  fourierdlem54  44408  fourierdlem63  44417  fourierdlem64  44418  fourierdlem65  44419  fourierdlem79  44433  fourierdlem102  44456  fourierdlem103  44457  fourierdlem104  44458  fourierdlem114  44468  elaa2lem  44481  etransclem4  44486  etransclem7  44489  etransclem8  44490  etransclem17  44499  etransclem18  44500  etransclem20  44502  etransclem23  44505  etransclem27  44509  etransclem31  44513  etransclem32  44514  etransclem35  44517  etransclem41  44523  etransclem46  44528  etransclem48  44530  iundjiun  44708  caratheodorylem1  44774  2elfz2melfz  45557  elfzelfzlble  45560  el1fzopredsuc  45564  iccpartiltu  45621  iccpartgt  45626  iccpartnel  45637  fargshiftfo  45641  altgsumbc  46435  altgsumbcALT  46436  nn0sumshdiglemA  46712  nn0sumshdiglemB  46713
  Copyright terms: Public domain W3C validator