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

Theorem elfzelz 12898
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 12894 . 2 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ𝑀))
2 eluzelz 12242 . 2 (𝐾 ∈ (ℤ𝑀) → 𝐾 ∈ ℤ)
31, 2syl 17 1 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cfv 6349  (class class class)co 7145  cz 11970  cuz 12232  ...cfz 12882
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 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583
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 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-fv 6357  df-ov 7148  df-oprab 7149  df-mpo 7150  df-1st 7680  df-2nd 7681  df-neg 10862  df-z 11971  df-uz 12233  df-fz 12883
This theorem is referenced by:  fzssz  12899  elfz1eq  12908  fzsplit2  12922  fzdisj  12924  elfznn  12926  ssfzunsnext  12942  fznatpl1  12951  fzrev2i  12962  fzrev3i  12964  fznuz  12979  fzrevral  12982  fzshftral  12985  fznn0sub2  13004  elfzmlbm  13007  difelfznle  13011  predfz  13022  fzosplit  13060  sermono  13392  seqf1olem1  13399  seqf1olem2  13400  bcval2  13655  bcval4  13657  bccmpl  13659  bcp1nk  13667  bcval5  13668  bcpasc  13671  bccl2  13673  seqcoll  13812  seqcoll2  13813  swrdval2  13998  swrdwrdsymb  14014  ccatswrd  14020  addlenrevpfx  14042  ccatpfx  14053  swrdswrd  14057  swrdpfx  14059  pfxccatin12lem2a  14079  pfxccatin12lem1  14080  swrdccatin2  14081  pfxccatin12lem2  14083  pfxccatin12  14085  spllen  14106  splfv1  14107  cshwidxm  14160  cshwidxn  14161  lswcshw  14167  2cshwcshw  14177  cshwcshid  14179  cshwcsh2id  14180  swrds2m  14293  seqshft  14434  sumrblem  15058  summolem2a  15062  fsum0diaglem  15121  mptfzshft  15123  fsumrev  15124  fsumshftm  15126  fsum0diag2  15128  binomlem  15174  binom11  15177  bcxmas  15180  arisum  15205  geo2sum  15219  mertenslem1  15230  prodfn0  15240  prodrblem  15273  prodmolem2a  15278  fprodntriv  15286  fprodser  15293  fprod1p  15312  fprodrev  15321  fallfacval3  15356  fallfacfwd  15380  0fallfac  15381  binomfallfaclem1  15383  binomfallfaclem2  15384  binomrisefac  15386  fallfacval4  15387  bpolycl  15396  bpolysum  15397  bpolydiflem  15398  fsumkthpow  15400  bpoly4  15403  fzm1ndvds  15662  pwp1fsum  15732  prmdvdsfz  16039  isprm7  16042  hashdvds  16102  phiprmpw  16103  prmdiveq  16113  prmdivdiv  16114  modprminv  16126  modprminveq  16127  modprm0  16132  4sqlem11  16281  4sqlem12  16282  vdwapun  16300  prmop1  16364  prmdvdsprmo  16368  prmdvdsprmop  16369  prmgaplem1  16375  prmgaplem2  16376  prmgaplcmlem1  16377  prmgaplcmlem2  16378  prmgapprmo  16388  cshwshashlem1  16419  cshwshashlem2  16420  dfod2  18622  efgredleme  18800  efgredlemc  18802  efgredlemb  18803  gsummptshft  18987  srgbinomlem3  19223  srgbinomlem4  19224  srgbinomlem  19225  chpscmatgsummon  21383  cayhamlem1  21404  iscmet3  23825  mbfi1fseqlem4  24248  itgz  24310  itgcl  24313  ibl0  24316  iblss  24334  iblss2  24335  itgss  24341  itgeqa  24343  iblconst  24347  iblabsr  24359  iblmulc2  24360  itgsplit  24365  dvfsumlem3  24554  plyeq0lem  24729  aalioulem1  24850  cxpeq  25265  birthdaylem2  25458  wilthlem1  25573  wilthlem2  25574  wilthlem3  25575  ftalem5  25582  basellem3  25588  basellem4  25589  dvdsppwf1o  25691  dvdsflf1o  25692  musum  25696  ppiub  25708  chtublem  25715  mersenne  25731  bposlem1  25788  lgsval2lem  25811  lgsdilem2  25837  lgsqrlem2  25851  lgsqrlem4  25853  gausslemma2dlem1a  25869  gausslemma2dlem1  25870  gausslemma2dlem3  25872  gausslemma2dlem4  25873  gausslemma2dlem5a  25874  gausslemma2dlem5  25875  gausslemma2dlem6  25876  lgseisenlem1  25879  lgseisenlem2  25880  lgseisenlem3  25881  lgsquadlem1  25884  lgsquadlem2  25885  lgsquadlem3  25886  2lgslem1a1  25893  2lgslem1a  25895  2lgslem1b  25896  rpvmasumlem  25991  dchrisumlem1  25993  dchrisumlem2  25994  dchrmusum2  25998  dchrvmasumlem1  25999  dchrvmasum2lem  26000  dchrvmasum2if  26001  dchrvmasumlem3  26003  dchrvmasumiflem1  26005  dchrvmasumiflem2  26006  dchrisum0flblem1  26012  rpvmasum2  26016  dchrisum0lem1b  26019  dchrisum0lem1  26020  dchrisum0lem2a  26021  dchrisum0lem2  26022  dchrisum0lem3  26023  dchrmusumlem  26026  dchrvmasumlem  26027  logdivbnd  26060  pntpbnd1  26090  pntlemh  26103  pntlemj  26107  pntlemf  26109  ostth2lem2  26138  axlowdimlem13  26668  axlowdimlem14  26669  axlowdimlem16  26671  crctcshlem4  27526  crctcshwlkn0  27527  erclwwlkeqlen  27725  clwwnisshclwwsn  27766  eleclclwwlknlem2  27768  erclwwlkneqlen  27775  fzm1ne1  30439  fzsplit3  30444  bcm1n  30445  fzone1  30450  prmdvdsbc  30459  swrdf1  30558  cycpmco2lem7  30702  freshmansdream  30787  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemodife  31655  ballotlemimin  31663  ballotlemsgt1  31668  ballotlemsel1i  31670  ballotlemsf1o  31671  ballotlemsi  31672  ballotlemsima  31673  ballotlemfg  31683  ballotlemfrc  31684  ballotlemfrceq  31686  ballotlemfrcn0  31687  ballotlemirc  31689  ballotlem1ri  31692  revpfxsfxrev  32260  swrdrevpfx  32261  pfxwlk  32268  swrdwlk  32271  erdszelem8  32343  erdszelem9  32344  cvmliftlem7  32436  supfz  32858  inffz  32859  bcprod  32868  fwddifnp1  33524  poimirlem1  34775  poimirlem2  34776  poimirlem7  34781  poimirlem14  34788  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem23  34797  poimirlem24  34798  poimirlem27  34801  poimirlem28  34802  poimirlem31  34805  poimirlem32  34806  mblfinlem2  34812  iblmulc2nc  34839  fdc  34903  irrapxlem1  39299  irrapxlem2  39300  irrapxlem3  39301  pellexlem5  39310  acongrep  39457  fzmaxdif  39458  acongeq  39460  jm2.22  39472  jm2.23  39473  jm2.26lem3  39478  jm2.26  39479  jm2.27dlem2  39487  hashnzfz  40532  monoords  41444  elfzelzd  41462  fmul01lt1lem1  41745  fmul01lt1lem2  41746  sumnnodd  41791  limsupubuzlem  41873  dvnmul  42108  dvnprodlem2  42112  iblsplit  42131  iblspltprt  42138  itgspltprt  42144  stoweidlem3  42169  stoweidlem11  42177  stoweidlem20  42186  stoweidlem26  42192  stoweidlem34  42200  stoweidlem59  42225  stirlinglem10  42249  dirkertrigeqlem1  42264  dirkertrigeqlem2  42265  dirkertrigeqlem3  42266  dirkertrigeq  42267  dirkeritg  42268  fourierdlem11  42284  fourierdlem12  42285  fourierdlem15  42288  fourierdlem34  42307  fourierdlem41  42314  fourierdlem46  42318  fourierdlem48  42320  fourierdlem49  42321  fourierdlem50  42322  fourierdlem54  42326  fourierdlem63  42335  fourierdlem64  42336  fourierdlem65  42337  fourierdlem79  42351  fourierdlem102  42374  fourierdlem103  42375  fourierdlem104  42376  fourierdlem114  42386  elaa2lem  42399  etransclem4  42404  etransclem7  42407  etransclem8  42408  etransclem17  42417  etransclem18  42418  etransclem20  42420  etransclem23  42423  etransclem27  42427  etransclem31  42431  etransclem32  42432  etransclem35  42435  etransclem41  42441  etransclem46  42446  etransclem48  42448  iundjiun  42623  caratheodorylem1  42689  2elfz2melfz  43399  elfzelfzlble  43402  el1fzopredsuc  43406  iccpartgtprec  43427  iccpartiltu  43429  iccpartgt  43434  iccpartnel  43445  fargshiftfo  43449  altgsumbc  44298  altgsumbcALT  44299  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578
  Copyright terms: Public domain W3C validator