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

Theorem elfzelz 11798
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  |-  ( K  e.  ( M ... N )  ->  K  e.  ZZ )

Proof of Theorem elfzelz
StepHypRef Expression
1 elfzuz 11794 . 2  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
2 eluzelz 11168 . 2  |-  ( K  e.  ( ZZ>= `  M
)  ->  K  e.  ZZ )
31, 2syl 17 1  |-  ( K  e.  ( M ... N )  ->  K  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   ` cfv 5601  (class class class)co 6305   ZZcz 10937   ZZ>=cuz 11159   ...cfz 11782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-cnex 9594  ax-resscn 9595
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-1st 6807  df-2nd 6808  df-neg 9862  df-z 10938  df-uz 11160  df-fz 11783
This theorem is referenced by:  fzssz  11799  elfz1eq  11808  fzsplit2  11822  fzdisj  11824  elfznn  11826  fznatpl1  11848  fzrev2i  11858  fzrev3i  11860  fznuz  11874  fzrevral  11877  fzshftral  11880  fznn0sub2  11895  elfzmlbm  11898  difelfznle  11903  predfz  11912  fzosplit  11949  sermono  12242  seqf1olem1  12249  seqf1olem2  12250  bcval2  12487  bcval4  12489  bccmpl  12491  bcp1nk  12499  bcval5  12500  bcpasc  12503  bccl2  12505  seqcoll  12621  seqcoll2  12622  swrdval2  12761  swrd0val  12762  addlenrevswrd  12778  swrd0fv  12780  ccatswrd  12797  swrdswrd  12801  swrdswrd0  12803  swrdccatin12lem2a  12826  swrdccatin12lem2b  12827  swrdccatin2  12828  swrdccatin12  12832  spllen  12846  splfv1  12847  cshwidxm  12894  cshwidxn  12895  lswcshw  12899  2cshwcshw  12909  cshwcshid  12911  cshwcsh2id  12912  seqshft  13127  sumrblem  13755  summolem2a  13759  fsum0diaglem  13815  mptfzshft  13817  fsumrev  13818  fsumshftm  13820  fsum0diag2  13822  binomlem  13865  binom11  13868  bcxmas  13871  arisum  13896  geo2sum  13907  mertenslem1  13918  prodfn0  13928  prodrblem  13961  prodmolem2a  13966  fprodntriv  13974  fprodser  13981  fprod1p  14000  fprodrev  14009  fallfacval3  14043  fallfacfwd  14067  0fallfac  14068  binomfallfaclem1  14070  binomfallfaclem2  14071  binomrisefac  14073  fallfacval4  14074  bpolycl  14083  bpolysum  14084  bpolydiflem  14085  fsumkthpow  14087  bpoly4  14090  fzm1ndvds  14335  prmdvdsfz  14620  hashdvds  14692  phiprmpw  14693  prmdiveq  14703  prmdivdiv  14704  modprminv  14713  modprminveq  14714  modprm0  14719  4sqlem11  14862  4sqlem12  14863  vdwapun  14887  prmop1  14959  prmdvdsprmo  14963  prmdvdsprmop  14964  prmgaplem1  14970  prmgaplem2  14971  prmgaplcmlem1  14972  prmgaplcmlem2  14973  prmgaplcmlem1OLD  14975  prmgaplcmlem2OLD  14976  prmdvdsprmorOLD  14978  prmdvdsprmorpOLD  14979  prmgapprmo  14996  cshwshashlem1  15029  cshwshashlem2  15030  dfod2  17153  efgredleme  17328  efgredlemc  17330  efgredlemb  17331  gsummptshft  17504  srgbinomlem3  17710  srgbinomlem4  17711  srgbinomlem  17712  chpscmatgsummon  19800  cayhamlem1  19821  iscmet3  22156  mbfi1fseqlem4  22553  itgz  22615  itgcl  22618  ibl0  22621  iblss  22639  iblss2  22640  itgss  22646  itgeqa  22648  iblconst  22652  iblabsr  22664  iblmulc2  22665  itgsplit  22670  dvfsumlem3  22857  plyeq0lem  23032  aalioulem1  23153  cxpeq  23562  birthdaylem2  23743  wilthlem1  23858  wilthlem2  23859  wilthlem3  23860  ftalem5  23866  basellem3  23872  basellem4  23873  dvdsppwf1o  23978  dvdsflf1o  23979  musum  23983  ppiub  23995  chtublem  24002  mersenne  24018  bposlem1  24075  lgsval2lem  24097  lgsdilem2  24122  lgsqrlem2  24133  lgsqrlem4  24135  lgseisenlem1  24140  lgseisenlem2  24141  lgseisenlem3  24142  lgsquadlem1  24145  lgsquadlem2  24146  lgsquadlem3  24147  rpvmasumlem  24188  dchrisumlem1  24190  dchrisumlem2  24191  dchrmusum2  24195  dchrvmasumlem1  24196  dchrvmasum2lem  24197  dchrvmasum2if  24198  dchrvmasumlem3  24200  dchrvmasumiflem1  24202  dchrvmasumiflem2  24203  dchrisum0flblem1  24209  rpvmasum2  24213  dchrisum0lem1b  24216  dchrisum0lem1  24217  dchrisum0lem2a  24218  dchrisum0lem2  24219  dchrisum0lem3  24220  dchrmusumlem  24223  dchrvmasumlem  24224  logdivbnd  24257  pntpbnd1  24287  pntlemh  24300  pntlemj  24304  pntlemf  24306  ostth2lem2  24335  axlowdimlem13  24830  axlowdimlem14  24831  axlowdimlem16  24833  fargshiftfo  25211  clwwnisshclwwn  25382  erclwwlkeqlen  25385  eleclclwwlknlem2  25391  erclwwlkneqlen  25397  clwlkfclwwlk  25417  fzsplit3  28206  bcm1n  28207  fz1fzo0m1  28215  ballotlemfc0  29151  ballotlemfcc  29152  ballotlemodife  29156  ballotlemimin  29164  ballotlemsgt1  29169  ballotlemsel1i  29171  ballotlemsf1o  29172  ballotlemsi  29173  ballotlemsima  29174  ballotlemfg  29184  ballotlemfrc  29185  ballotlemfrceq  29187  ballotlemfrcn0  29188  ballotlemirc  29190  ballotlem1ri  29193  erdszelem8  29709  erdszelem9  29710  cvmliftlem7  29802  supfz  30149  inffz  30150  bcprod  30161  fwddifnp1  30717  poimirlem1  31644  poimirlem2  31645  poimirlem7  31650  poimirlem14  31657  poimirlem15  31658  poimirlem16  31659  poimirlem17  31660  poimirlem19  31662  poimirlem20  31663  poimirlem23  31666  poimirlem24  31667  poimirlem27  31670  poimirlem28  31671  poimirlem31  31674  poimirlem32  31675  mblfinlem2  31681  iblmulc2nc  31710  fdc  31777  irrapxlem1  35375  irrapxlem2  35376  irrapxlem3  35377  pellexlem5  35386  acongrep  35535  fzmaxdif  35536  acongeq  35538  jm2.22  35555  jm2.23  35556  jm2.26lem3  35561  jm2.26  35562  jm2.27dlem2  35570  isprm7  36296  hashnzfz  36305  monoords  37122  elfzelzd  37144  fmul01lt1lem1  37233  fmul01lt1lem2  37234  sumnnodd  37281  dvnmul  37386  dvnprodlem2  37390  iblsplit  37411  iblspltprt  37418  itgspltprt  37424  stoweidlem3  37431  stoweidlem11  37439  stoweidlem20  37448  stoweidlem26  37454  stoweidlem34  37463  stoweidlem59  37488  stirlinglem10  37513  dirkertrigeqlem1  37528  dirkertrigeqlem2  37529  dirkertrigeqlem3  37530  dirkertrigeq  37531  dirkeritg  37532  fourierdlem11  37548  fourierdlem12  37549  fourierdlem15  37552  fourierdlem34  37571  fourierdlem41  37578  fourierdlem46  37583  fourierdlem48  37585  fourierdlem49  37586  fourierdlem50  37587  fourierdlem54  37591  fourierdlem63  37600  fourierdlem64  37601  fourierdlem65  37602  fourierdlem79  37616  fourierdlem102  37639  fourierdlem103  37640  fourierdlem104  37641  fourierdlem114  37651  elaa2lem  37664  etransclem4  37669  etransclem7  37672  etransclem8  37673  etransclem17  37682  etransclem18  37683  etransclem20  37685  etransclem23  37688  etransclem27  37692  etransclem31  37696  etransclem32  37697  etransclem35  37700  etransclem41  37706  etransclem46  37711  etransclem48  37713  iundjiun  37806  caratheodorylem1  37855  el1fzopredsuc  38111  iccpartgtprec  38123  iccpartiltu  38125  iccpartgt  38130  iccpartnel  38141  addlenrevpfx  38327  ccatpfx  38339  pfxccatin12lem1  38353  pfxccatin12lem2  38354  pfxccatin12  38355  2elfz2melfz  38406  elfzelfzlble  38409  altgsumbc  38892  altgsumbcALT  38893  nn0sumshdiglemA  39190  nn0sumshdiglemB  39191
  Copyright terms: Public domain W3C validator