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

Theorem elfzelz 11023
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 11019 . 2  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
2 eluzelz 10460 . 2  |-  ( K  e.  ( ZZ>= `  M
)  ->  K  e.  ZZ )
31, 2syl 16 1  |-  ( K  e.  ( M ... N )  ->  K  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   ` cfv 5421  (class class class)co 6048   ZZcz 10246   ZZ>=cuz 10452   ...cfz 11007
This theorem is referenced by:  elfz1eq  11032  fzsplit2  11040  fzdisj  11042  elfznn  11044  fznn0sub2  11050  fzrev2i  11074  fzrev3i  11076  fznuz  11092  fzrevral  11094  fzshftral  11097  fzosplit  11129  sermono  11318  seqf1olem1  11325  seqf1olem2  11326  bcval2  11559  bcval4  11561  bccmpl  11563  bcm1k  11569  bcp1nk  11571  bcval5  11572  bcpasc  11575  bccl2  11577  seqcoll  11675  seqcoll2  11676  swrdval2  11730  swrd0val  11731  ccatswrd  11736  spllen  11746  splfv1  11747  seqshft  11863  sumrblem  12468  summolem2a  12472  fsum0diaglem  12523  fsumrev  12525  fsumshft  12526  fsumshftm  12527  fsum0diag2  12529  binomlem  12571  binom11  12574  bcxmas  12578  arisum  12602  geo2sum  12613  mertenslem1  12624  fzm1ndvds  12864  hashdvds  13127  phiprmpw  13128  prmdiveq  13138  prmdivdiv  13139  4sqlem11  13286  4sqlem12  13287  vdwapun  13305  dfod2  15163  efgredleme  15338  efgredlemc  15340  efgredlemb  15341  iscmet3  19207  mbfi1fseqlem4  19571  itgz  19633  itgcl  19636  ibl0  19639  iblss  19657  iblss2  19658  itgss  19664  itgeqa  19666  iblconst  19670  iblabsr  19682  iblmulc2  19683  itgsplit  19688  dvfsumlem3  19873  plyeq0lem  20090  aalioulem1  20210  cxpeq  20602  birthdaylem2  20752  wilthlem1  20812  wilthlem2  20813  wilthlem3  20814  ftalem5  20820  basellem3  20826  basellem4  20827  dvdsppwf1o  20932  dvdsflf1o  20933  musum  20937  ppiub  20949  chtublem  20956  mersenne  20972  bposlem1  21029  lgsval2lem  21051  lgsdilem2  21076  lgsqrlem2  21087  lgsqrlem4  21089  lgseisenlem1  21094  lgseisenlem2  21095  lgseisenlem3  21096  lgsquadlem1  21099  lgsquadlem2  21100  lgsquadlem3  21101  rpvmasumlem  21142  dchrisumlem1  21144  dchrisumlem2  21145  dchrmusum2  21149  dchrvmasumlem1  21150  dchrvmasum2lem  21151  dchrvmasum2if  21152  dchrvmasumlem3  21154  dchrvmasumiflem1  21156  dchrvmasumiflem2  21157  dchrisum0flblem1  21163  rpvmasum2  21167  dchrisum0lem1b  21170  dchrisum0lem1  21171  dchrisum0lem2a  21172  dchrisum0lem2  21173  dchrisum0lem3  21174  dchrmusumlem  21177  dchrvmasumlem  21178  logdivbnd  21211  pntpbnd1  21241  pntlemh  21254  pntlemj  21258  pntlemf  21260  ostth2lem2  21289  fargshiftfo  21586  fzsplit3  24111  bcm1n  24112  ballotlemfc0  24711  ballotlemfcc  24712  ballotlemodife  24716  ballotlemimin  24724  ballotlemsgt1  24729  ballotlemsel1i  24731  ballotlemsf1o  24732  ballotlemsi  24733  ballotlemsima  24734  ballotlemfg  24744  ballotlemfrc  24745  ballotlemfrceq  24747  ballotlemfrcn0  24748  ballotlemirc  24750  ballotlem1ri  24753  erdszelem8  24845  erdszelem9  24846  cvmliftlem7  24939  fznatpl1  25159  supfz  25160  inffz  25161  prodfn0  25183  prodrblem  25216  prodmolem2a  25221  fprodntriv  25229  fprodser  25236  fprod1p  25252  fprodshft  25261  fprodrev  25262  fallfacfwd  25311  0fallfac  25312  binomfallfaclem1  25314  binomfallfaclem2  25315  binomrisefac  25317  predfz  25425  axlowdimlem13  25805  axlowdimlem14  25806  axlowdimlem16  25808  bpolycl  26010  bpolysum  26011  bpolydiflem  26012  fsumkthpow  26014  bpoly4  26017  mblfinlem  26151  iblmulc2nc  26177  fdc  26347  irrapxlem1  26783  irrapxlem2  26784  irrapxlem3  26785  pellexlem5  26794  acongrep  26943  fzmaxdif  26944  acongeq  26946  jm2.22  26964  jm2.23  26965  jm2.26lem3  26970  jm2.26  26971  jm2.27dlem2  26979  fmul01lt1lem1  27589  fmul01lt1lem2  27590  stoweidlem3  27627  stoweidlem11  27635  stoweidlem20  27644  stoweidlem26  27650  stoweidlem34  27658  stoweidlem59  27683  stirlinglem10  27707  addlenrevswrd  28012  swrd0swrd  28017  swrdswrd  28019  swrd0swrdid  28020  swrdswrd0  28021  swrdccatin2lem1  28025  swrdccatin12lem3a  28029  swrdccatin12lem3b  28030  swrdccatin12b  28035  swrdccatin12c  28036  swrdccat3b  28039
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-cnex 9010  ax-resscn 9011
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-fv 5429  df-ov 6051  df-oprab 6052  df-mpt2 6053  df-1st 6316  df-2nd 6317  df-neg 9258  df-z 10247  df-uz 10453  df-fz 11008
  Copyright terms: Public domain W3C validator