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

Theorem elfzelz 11554
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 11550 . 2  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
2 eluzelz 10971 . 2  |-  ( K  e.  ( ZZ>= `  M
)  ->  K  e.  ZZ )
31, 2syl 16 1  |-  ( K  e.  ( M ... N )  ->  K  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   ` cfv 5516  (class class class)co 6190   ZZcz 10747   ZZ>=cuz 10962   ...cfz 11538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-cnex 9439  ax-resscn 9440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-iun 4271  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-fv 5524  df-ov 6193  df-oprab 6194  df-mpt2 6195  df-1st 6677  df-2nd 6678  df-neg 9699  df-z 10748  df-uz 10963  df-fz 11539
This theorem is referenced by:  elfz1eq  11563  fzsplit2  11575  fzdisj  11577  elfznn  11579  fznn0sub2  11589  fznatpl1  11611  fzrev2i  11622  fzrev3i  11624  fznuz  11643  fzrevral  11645  fzshftral  11648  fzosplit  11683  sermono  11939  seqf1olem1  11946  seqf1olem2  11947  bcval2  12182  bcval4  12184  bccmpl  12186  bcm1k  12192  bcp1nk  12194  bcval5  12195  bcpasc  12198  bccl2  12200  seqcoll  12318  seqcoll2  12319  swrdval2  12418  swrd0val  12419  addlenrevswrd  12432  swrd0fv  12437  ccatswrd  12452  swrdswrd  12456  swrdswrd0  12458  swrdccatin12lem2a  12478  swrdccatin12lem2b  12479  swrdccatin2  12480  swrdccatin12  12484  spllen  12498  splfv1  12499  cshwidxm  12546  cshwidxn  12547  lswcshw  12551  seqshft  12676  sumrblem  13290  summolem2a  13294  fsum0diaglem  13345  mptfzshft  13347  fsumrev  13348  fsumshftm  13350  fsum0diag2  13352  binomlem  13394  binom11  13397  bcxmas  13400  arisum  13424  geo2sum  13435  mertenslem1  13446  fzm1ndvds  13687  hashdvds  13952  phiprmpw  13953  prmdiveq  13963  prmdivdiv  13964  modprminv  13972  modprminveq  13973  modprm0  13975  4sqlem11  14118  4sqlem12  14119  vdwapun  14137  cshwshashlem1  14224  cshwshashlem2  14225  dfod2  16169  efgredleme  16344  efgredlemc  16346  efgredlemb  16347  gsummptshft  16534  srgbinomlem3  16746  srgbinomlem4  16747  srgbinomlem  16748  iscmet3  20920  mbfi1fseqlem4  21312  itgz  21374  itgcl  21377  ibl0  21380  iblss  21398  iblss2  21399  itgss  21405  itgeqa  21407  iblconst  21411  iblabsr  21423  iblmulc2  21424  itgsplit  21429  dvfsumlem3  21616  plyeq0lem  21794  aalioulem1  21914  cxpeq  22311  birthdaylem2  22462  wilthlem1  22522  wilthlem2  22523  wilthlem3  22524  ftalem5  22530  basellem3  22536  basellem4  22537  dvdsppwf1o  22642  dvdsflf1o  22643  musum  22647  ppiub  22659  chtublem  22666  mersenne  22682  bposlem1  22739  lgsval2lem  22761  lgsdilem2  22786  lgsqrlem2  22797  lgsqrlem4  22799  lgseisenlem1  22804  lgseisenlem2  22805  lgseisenlem3  22806  lgsquadlem1  22809  lgsquadlem2  22810  lgsquadlem3  22811  rpvmasumlem  22852  dchrisumlem1  22854  dchrisumlem2  22855  dchrmusum2  22859  dchrvmasumlem1  22860  dchrvmasum2lem  22861  dchrvmasum2if  22862  dchrvmasumlem3  22864  dchrvmasumiflem1  22866  dchrvmasumiflem2  22867  dchrisum0flblem1  22873  rpvmasum2  22877  dchrisum0lem1b  22880  dchrisum0lem1  22881  dchrisum0lem2a  22882  dchrisum0lem2  22883  dchrisum0lem3  22884  dchrmusumlem  22887  dchrvmasumlem  22888  logdivbnd  22921  pntpbnd1  22951  pntlemh  22964  pntlemj  22968  pntlemf  22970  ostth2lem2  22999  axlowdimlem13  23335  axlowdimlem14  23336  axlowdimlem16  23338  fargshiftfo  23659  fzsplit3  26212  bcm1n  26213  ballotlemfc0  27009  ballotlemfcc  27010  ballotlemodife  27014  ballotlemimin  27022  ballotlemsgt1  27027  ballotlemsel1i  27029  ballotlemsf1o  27030  ballotlemsi  27031  ballotlemsima  27032  ballotlemfg  27042  ballotlemfrc  27043  ballotlemfrceq  27045  ballotlemfrcn0  27046  ballotlemirc  27048  ballotlem1ri  27051  erdszelem8  27220  erdszelem9  27221  cvmliftlem7  27314  supfz  27520  inffz  27521  prodfn0  27543  prodrblem  27576  prodmolem2a  27581  fprodntriv  27589  fprodser  27596  fprod1p  27612  fprodshft  27621  fprodrev  27622  fallfacval3  27649  fallfacfwd  27673  0fallfac  27674  binomfallfaclem1  27676  binomfallfaclem2  27677  binomrisefac  27679  fallfacval4  27680  predfz  27798  bpolycl  28329  bpolysum  28330  bpolydiflem  28331  fsumkthpow  28333  bpoly4  28336  mblfinlem2  28567  iblmulc2nc  28595  fdc  28779  irrapxlem1  29301  irrapxlem2  29302  irrapxlem3  29303  pellexlem5  29312  acongrep  29461  fzmaxdif  29462  acongeq  29464  jm2.22  29482  jm2.23  29483  jm2.26lem3  29488  jm2.26  29489  jm2.27dlem2  29497  fmul01lt1lem1  29903  fmul01lt1lem2  29904  stoweidlem3  29936  stoweidlem11  29944  stoweidlem20  29953  stoweidlem26  29959  stoweidlem34  29967  stoweidlem59  29992  stirlinglem10  30016  2elfz2melfz  30340  elfzelfzlble  30347  clwwnisshclwwn  30611  erclwwlksym0  30616  erclwwlktr0  30617  erclwwlkeqlen  30620  difelfznle  30626  cshwlemma1  30627  eleclclwwlknlem2  30629  erclwwlkneqlen  30636  clwlkfclwwlk  30655  altgsumbc  30887  altgsumbcALT  30888  cpscmatgsummon  31299  cayhamlem1  31320
  Copyright terms: Public domain W3C validator