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

Theorem elfzelz 12896
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
StepHypRef Expression
1 elfzuz 12892 . 2 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ𝑀))
2 eluzelz 12241 . 2 (𝐾 ∈ (ℤ𝑀) → 𝐾 ∈ ℤ)
31, 2syl 17 1 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cfv 6348  (class class class)co 7145  cz 11969  cuz 12231  ...cfz 12880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-1st 7678  df-2nd 7679  df-neg 10861  df-z 11970  df-uz 12232  df-fz 12881
This theorem is referenced by:  fzssz  12897  elfz1eq  12906  fzsplit2  12920  fzdisj  12922  elfznn  12924  ssfzunsnext  12940  fznatpl1  12949  fzrev2i  12960  fzrev3i  12962  fznuz  12977  fzrevral  12980  fzshftral  12983  fznn0sub2  13002  elfzmlbm  13005  difelfznle  13009  predfz  13020  fzosplit  13058  sermono  13390  seqf1olem1  13397  seqf1olem2  13398  bcval2  13653  bcval4  13655  bccmpl  13657  bcp1nk  13665  bcval5  13666  bcpasc  13669  bccl2  13671  seqcoll  13810  seqcoll2  13811  swrdval2  13996  swrdwrdsymb  14012  ccatswrd  14018  addlenrevpfx  14040  ccatpfx  14051  swrdswrd  14055  swrdpfx  14057  pfxccatin12lem2a  14077  pfxccatin12lem1  14078  swrdccatin2  14079  pfxccatin12lem2  14081  pfxccatin12  14083  spllen  14104  splfv1  14105  cshwidxm  14158  cshwidxn  14159  lswcshw  14165  2cshwcshw  14175  cshwcshid  14177  cshwcsh2id  14178  swrds2m  14291  seqshft  14432  sumrblem  15056  summolem2a  15060  fsum0diaglem  15119  mptfzshft  15121  fsumrev  15122  fsumshftm  15124  fsum0diag2  15126  binomlem  15172  binom11  15175  bcxmas  15178  arisum  15203  geo2sum  15217  mertenslem1  15228  prodfn0  15238  prodrblem  15271  prodmolem2a  15276  fprodntriv  15284  fprodser  15291  fprod1p  15310  fprodrev  15319  fallfacval3  15354  fallfacfwd  15378  0fallfac  15379  binomfallfaclem1  15381  binomfallfaclem2  15382  binomrisefac  15384  fallfacval4  15385  bpolycl  15394  bpolysum  15395  bpolydiflem  15396  fsumkthpow  15398  bpoly4  15401  fzm1ndvds  15660  pwp1fsum  15730  prmdvdsfz  16037  isprm7  16040  hashdvds  16100  phiprmpw  16101  prmdiveq  16111  prmdivdiv  16112  modprminv  16124  modprminveq  16125  modprm0  16130  4sqlem11  16279  4sqlem12  16280  vdwapun  16298  prmop1  16362  prmdvdsprmo  16366  prmdvdsprmop  16367  prmgaplem1  16373  prmgaplem2  16374  prmgaplcmlem1  16375  prmgaplcmlem2  16376  prmgapprmo  16386  cshwshashlem1  16417  cshwshashlem2  16418  dfod2  18620  efgredleme  18798  efgredlemc  18800  efgredlemb  18801  gsummptshft  18985  srgbinomlem3  19221  srgbinomlem4  19222  srgbinomlem  19223  chpscmatgsummon  21381  cayhamlem1  21402  iscmet3  23823  mbfi1fseqlem4  24246  itgz  24308  itgcl  24311  ibl0  24314  iblss  24332  iblss2  24333  itgss  24339  itgeqa  24341  iblconst  24345  iblabsr  24357  iblmulc2  24358  itgsplit  24363  dvfsumlem3  24552  plyeq0lem  24727  aalioulem1  24848  cxpeq  25265  birthdaylem2  25457  wilthlem1  25572  wilthlem2  25573  wilthlem3  25574  ftalem5  25581  basellem3  25587  basellem4  25588  dvdsppwf1o  25690  dvdsflf1o  25691  musum  25695  ppiub  25707  chtublem  25714  mersenne  25730  bposlem1  25787  lgsval2lem  25810  lgsdilem2  25836  lgsqrlem2  25850  lgsqrlem4  25852  gausslemma2dlem1a  25868  gausslemma2dlem1  25869  gausslemma2dlem3  25871  gausslemma2dlem4  25872  gausslemma2dlem5a  25873  gausslemma2dlem5  25874  gausslemma2dlem6  25875  lgseisenlem1  25878  lgseisenlem2  25879  lgseisenlem3  25880  lgsquadlem1  25883  lgsquadlem2  25884  lgsquadlem3  25885  2lgslem1a1  25892  2lgslem1a  25894  2lgslem1b  25895  rpvmasumlem  25990  dchrisumlem1  25992  dchrisumlem2  25993  dchrmusum2  25997  dchrvmasumlem1  25998  dchrvmasum2lem  25999  dchrvmasum2if  26000  dchrvmasumlem3  26002  dchrvmasumiflem1  26004  dchrvmasumiflem2  26005  dchrisum0flblem1  26011  rpvmasum2  26015  dchrisum0lem1b  26018  dchrisum0lem1  26019  dchrisum0lem2a  26020  dchrisum0lem2  26021  dchrisum0lem3  26022  dchrmusumlem  26025  dchrvmasumlem  26026  logdivbnd  26059  pntpbnd1  26089  pntlemh  26102  pntlemj  26106  pntlemf  26108  ostth2lem2  26137  axlowdimlem13  26667  axlowdimlem14  26668  axlowdimlem16  26670  crctcshlem4  27525  crctcshwlkn0  27526  erclwwlkeqlen  27724  clwwnisshclwwsn  27765  eleclclwwlknlem2  27767  erclwwlkneqlen  27774  fzm1ne1  30438  fzsplit3  30443  bcm1n  30444  fzone1  30449  prmdvdsbc  30458  swrdf1  30557  cycpmco2lem7  30701  freshmansdream  30786  ballotlemfc0  31649  ballotlemfcc  31650  ballotlemodife  31654  ballotlemimin  31662  ballotlemsgt1  31667  ballotlemsel1i  31669  ballotlemsf1o  31670  ballotlemsi  31671  ballotlemsima  31672  ballotlemfg  31682  ballotlemfrc  31683  ballotlemfrceq  31685  ballotlemfrcn0  31686  ballotlemirc  31688  ballotlem1ri  31691  revpfxsfxrev  32259  swrdrevpfx  32260  pfxwlk  32267  swrdwlk  32270  erdszelem8  32342  erdszelem9  32343  cvmliftlem7  32435  supfz  32857  inffz  32858  bcprod  32867  fwddifnp1  33523  poimirlem1  34774  poimirlem2  34775  poimirlem7  34780  poimirlem14  34787  poimirlem15  34788  poimirlem16  34789  poimirlem17  34790  poimirlem19  34792  poimirlem20  34793  poimirlem23  34796  poimirlem24  34797  poimirlem27  34800  poimirlem28  34801  poimirlem31  34804  poimirlem32  34805  mblfinlem2  34811  iblmulc2nc  34838  fdc  34901  irrapxlem1  39297  irrapxlem2  39298  irrapxlem3  39299  pellexlem5  39308  acongrep  39455  fzmaxdif  39456  acongeq  39458  jm2.22  39470  jm2.23  39471  jm2.26lem3  39476  jm2.26  39477  jm2.27dlem2  39485  hashnzfz  40529  monoords  41440  elfzelzd  41458  fmul01lt1lem1  41741  fmul01lt1lem2  41742  sumnnodd  41787  limsupubuzlem  41869  dvnmul  42104  dvnprodlem2  42108  iblsplit  42127  iblspltprt  42134  itgspltprt  42140  stoweidlem3  42165  stoweidlem11  42173  stoweidlem20  42182  stoweidlem26  42188  stoweidlem34  42196  stoweidlem59  42221  stirlinglem10  42245  dirkertrigeqlem1  42260  dirkertrigeqlem2  42261  dirkertrigeqlem3  42262  dirkertrigeq  42263  dirkeritg  42264  fourierdlem11  42280  fourierdlem12  42281  fourierdlem15  42284  fourierdlem34  42303  fourierdlem41  42310  fourierdlem46  42314  fourierdlem48  42316  fourierdlem49  42317  fourierdlem50  42318  fourierdlem54  42322  fourierdlem63  42331  fourierdlem64  42332  fourierdlem65  42333  fourierdlem79  42347  fourierdlem102  42370  fourierdlem103  42371  fourierdlem104  42372  fourierdlem114  42382  elaa2lem  42395  etransclem4  42400  etransclem7  42403  etransclem8  42404  etransclem17  42413  etransclem18  42414  etransclem20  42416  etransclem23  42419  etransclem27  42423  etransclem31  42427  etransclem32  42428  etransclem35  42431  etransclem41  42437  etransclem46  42442  etransclem48  42444  iundjiun  42619  caratheodorylem1  42685  2elfz2melfz  43395  elfzelfzlble  43398  el1fzopredsuc  43402  iccpartgtprec  43457  iccpartiltu  43459  iccpartgt  43464  iccpartnel  43475  fargshiftfo  43479  altgsumbc  44328  altgsumbcALT  44329  nn0sumshdiglemA  44607  nn0sumshdiglemB  44608
  Copyright terms: Public domain W3C validator