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 2107  cfv 6352  (class class class)co 7148  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 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-cnex 10582  ax-resscn 10583
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-fv 6360  df-ov 7151  df-oprab 7152  df-mpo 7153  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  18611  efgredleme  18789  efgredlemc  18791  efgredlemb  18792  gsummptshft  18976  srgbinomlem3  19212  srgbinomlem4  19213  srgbinomlem  19214  chpscmatgsummon  21369  cayhamlem1  21390  iscmet3  23811  mbfi1fseqlem4  24234  itgz  24296  itgcl  24299  ibl0  24302  iblss  24320  iblss2  24321  itgss  24327  itgeqa  24329  iblconst  24333  iblabsr  24345  iblmulc2  24346  itgsplit  24351  dvfsumlem3  24540  plyeq0lem  24715  aalioulem1  24836  cxpeq  25251  birthdaylem2  25444  wilthlem1  25559  wilthlem2  25560  wilthlem3  25561  ftalem5  25568  basellem3  25574  basellem4  25575  dvdsppwf1o  25677  dvdsflf1o  25678  musum  25682  ppiub  25694  chtublem  25701  mersenne  25717  bposlem1  25774  lgsval2lem  25797  lgsdilem2  25823  lgsqrlem2  25837  lgsqrlem4  25839  gausslemma2dlem1a  25855  gausslemma2dlem1  25856  gausslemma2dlem3  25858  gausslemma2dlem4  25859  gausslemma2dlem5a  25860  gausslemma2dlem5  25861  gausslemma2dlem6  25862  lgseisenlem1  25865  lgseisenlem2  25866  lgseisenlem3  25867  lgsquadlem1  25870  lgsquadlem2  25871  lgsquadlem3  25872  2lgslem1a1  25879  2lgslem1a  25881  2lgslem1b  25882  rpvmasumlem  25977  dchrisumlem1  25979  dchrisumlem2  25980  dchrmusum2  25984  dchrvmasumlem1  25985  dchrvmasum2lem  25986  dchrvmasum2if  25987  dchrvmasumlem3  25989  dchrvmasumiflem1  25991  dchrvmasumiflem2  25992  dchrisum0flblem1  25998  rpvmasum2  26002  dchrisum0lem1b  26005  dchrisum0lem1  26006  dchrisum0lem2a  26007  dchrisum0lem2  26008  dchrisum0lem3  26009  dchrmusumlem  26012  dchrvmasumlem  26013  logdivbnd  26046  pntpbnd1  26076  pntlemh  26089  pntlemj  26093  pntlemf  26095  ostth2lem2  26124  axlowdimlem13  26654  axlowdimlem14  26655  axlowdimlem16  26657  crctcshlem4  27512  crctcshwlkn0  27513  erclwwlkeqlen  27711  clwwnisshclwwsn  27752  eleclclwwlknlem2  27754  erclwwlkneqlen  27761  fzm1ne1  30425  fzsplit3  30430  bcm1n  30431  fzone1  30436  prmdvdsbc  30445  swrdf1  30544  cycpmco2lem7  30688  freshmansdream  30773  ballotlemfc0  31636  ballotlemfcc  31637  ballotlemodife  31641  ballotlemimin  31649  ballotlemsgt1  31654  ballotlemsel1i  31656  ballotlemsf1o  31657  ballotlemsi  31658  ballotlemsima  31659  ballotlemfg  31669  ballotlemfrc  31670  ballotlemfrceq  31672  ballotlemfrcn0  31673  ballotlemirc  31675  ballotlem1ri  31678  revpfxsfxrev  32246  swrdrevpfx  32247  pfxwlk  32254  swrdwlk  32257  erdszelem8  32329  erdszelem9  32330  cvmliftlem7  32422  supfz  32844  inffz  32845  bcprod  32854  fwddifnp1  33510  poimirlem1  34760  poimirlem2  34761  poimirlem7  34766  poimirlem14  34773  poimirlem15  34774  poimirlem16  34775  poimirlem17  34776  poimirlem19  34778  poimirlem20  34779  poimirlem23  34782  poimirlem24  34783  poimirlem27  34786  poimirlem28  34787  poimirlem31  34790  poimirlem32  34791  mblfinlem2  34797  iblmulc2nc  34824  fdc  34888  irrapxlem1  39284  irrapxlem2  39285  irrapxlem3  39286  pellexlem5  39295  acongrep  39442  fzmaxdif  39443  acongeq  39445  jm2.22  39457  jm2.23  39458  jm2.26lem3  39463  jm2.26  39464  jm2.27dlem2  39472  hashnzfz  40517  monoords  41429  elfzelzd  41447  fmul01lt1lem1  41730  fmul01lt1lem2  41731  sumnnodd  41776  limsupubuzlem  41858  dvnmul  42093  dvnprodlem2  42097  iblsplit  42116  iblspltprt  42123  itgspltprt  42129  stoweidlem3  42154  stoweidlem11  42162  stoweidlem20  42171  stoweidlem26  42177  stoweidlem34  42185  stoweidlem59  42210  stirlinglem10  42234  dirkertrigeqlem1  42249  dirkertrigeqlem2  42250  dirkertrigeqlem3  42251  dirkertrigeq  42252  dirkeritg  42253  fourierdlem11  42269  fourierdlem12  42270  fourierdlem15  42273  fourierdlem34  42292  fourierdlem41  42299  fourierdlem46  42303  fourierdlem48  42305  fourierdlem49  42306  fourierdlem50  42307  fourierdlem54  42311  fourierdlem63  42320  fourierdlem64  42321  fourierdlem65  42322  fourierdlem79  42336  fourierdlem102  42359  fourierdlem103  42360  fourierdlem104  42361  fourierdlem114  42371  elaa2lem  42384  etransclem4  42389  etransclem7  42392  etransclem8  42393  etransclem17  42402  etransclem18  42403  etransclem20  42405  etransclem23  42408  etransclem27  42412  etransclem31  42416  etransclem32  42417  etransclem35  42420  etransclem41  42426  etransclem46  42431  etransclem48  42433  iundjiun  42608  caratheodorylem1  42674  2elfz2melfz  43384  elfzelfzlble  43387  el1fzopredsuc  43391  iccpartgtprec  43412  iccpartiltu  43414  iccpartgt  43419  iccpartnel  43430  fargshiftfo  43434  altgsumbc  44232  altgsumbcALT  44233  nn0sumshdiglemA  44511  nn0sumshdiglemB  44512
  Copyright terms: Public domain W3C validator