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

Theorem elfzelz 11445
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 11441 . 2  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
2 eluzelz 10862 . 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 1756   ` cfv 5413  (class class class)co 6086   ZZcz 10638   ZZ>=cuz 10853   ...cfz 11429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-1st 6572  df-2nd 6573  df-neg 9590  df-z 10639  df-uz 10854  df-fz 11430
This theorem is referenced by:  elfz1eq  11454  fzsplit2  11466  fzdisj  11468  elfznn  11470  fznn0sub2  11480  fznatpl1  11502  fzrev2i  11513  fzrev3i  11515  fznuz  11534  fzrevral  11536  fzshftral  11539  fzosplit  11574  sermono  11830  seqf1olem1  11837  seqf1olem2  11838  bcval2  12073  bcval4  12075  bccmpl  12077  bcm1k  12083  bcp1nk  12085  bcval5  12086  bcpasc  12089  bccl2  12091  seqcoll  12208  seqcoll2  12209  swrdval2  12308  swrd0val  12309  addlenrevswrd  12322  swrd0fv  12327  ccatswrd  12342  swrdswrd  12346  swrdswrd0  12348  swrdccatin12lem2a  12368  swrdccatin12lem2b  12369  swrdccatin2  12370  swrdccatin12  12374  spllen  12388  splfv1  12389  cshwidxm  12436  cshwidxn  12437  lswcshw  12441  seqshft  12566  sumrblem  13180  summolem2a  13184  fsum0diaglem  13235  mptfzshft  13237  fsumrev  13238  fsumshftm  13240  fsum0diag2  13242  binomlem  13284  binom11  13287  bcxmas  13290  arisum  13314  geo2sum  13325  mertenslem1  13336  fzm1ndvds  13577  hashdvds  13842  phiprmpw  13843  prmdiveq  13853  prmdivdiv  13854  modprminv  13862  modprminveq  13863  modprm0  13865  4sqlem11  14008  4sqlem12  14009  vdwapun  14027  cshwshashlem1  14114  cshwshashlem2  14115  dfod2  16056  efgredleme  16231  efgredlemc  16233  efgredlemb  16234  gsummptshft  16419  srgbinomlem3  16630  srgbinomlem4  16631  srgbinomlem  16632  iscmet3  20784  mbfi1fseqlem4  21176  itgz  21238  itgcl  21241  ibl0  21244  iblss  21262  iblss2  21263  itgss  21269  itgeqa  21271  iblconst  21275  iblabsr  21287  iblmulc2  21288  itgsplit  21293  dvfsumlem3  21480  plyeq0lem  21658  aalioulem1  21778  cxpeq  22175  birthdaylem2  22326  wilthlem1  22386  wilthlem2  22387  wilthlem3  22388  ftalem5  22394  basellem3  22400  basellem4  22401  dvdsppwf1o  22506  dvdsflf1o  22507  musum  22511  ppiub  22523  chtublem  22530  mersenne  22546  bposlem1  22603  lgsval2lem  22625  lgsdilem2  22650  lgsqrlem2  22661  lgsqrlem4  22663  lgseisenlem1  22668  lgseisenlem2  22669  lgseisenlem3  22670  lgsquadlem1  22673  lgsquadlem2  22674  lgsquadlem3  22675  rpvmasumlem  22716  dchrisumlem1  22718  dchrisumlem2  22719  dchrmusum2  22723  dchrvmasumlem1  22724  dchrvmasum2lem  22725  dchrvmasum2if  22726  dchrvmasumlem3  22728  dchrvmasumiflem1  22730  dchrvmasumiflem2  22731  dchrisum0flblem1  22737  rpvmasum2  22741  dchrisum0lem1b  22744  dchrisum0lem1  22745  dchrisum0lem2a  22746  dchrisum0lem2  22747  dchrisum0lem3  22748  dchrmusumlem  22751  dchrvmasumlem  22752  logdivbnd  22785  pntpbnd1  22815  pntlemh  22828  pntlemj  22832  pntlemf  22834  ostth2lem2  22863  axlowdimlem13  23168  axlowdimlem14  23169  axlowdimlem16  23171  fargshiftfo  23492  fzsplit3  26046  bcm1n  26047  ballotlemfc0  26844  ballotlemfcc  26845  ballotlemodife  26849  ballotlemimin  26857  ballotlemsgt1  26862  ballotlemsel1i  26864  ballotlemsf1o  26865  ballotlemsi  26866  ballotlemsima  26867  ballotlemfg  26877  ballotlemfrc  26878  ballotlemfrceq  26880  ballotlemfrcn0  26881  ballotlemirc  26883  ballotlem1ri  26886  erdszelem8  27055  erdszelem9  27056  cvmliftlem7  27149  supfz  27355  inffz  27356  prodfn0  27378  prodrblem  27411  prodmolem2a  27416  fprodntriv  27424  fprodser  27431  fprod1p  27447  fprodshft  27456  fprodrev  27457  fallfacval3  27484  fallfacfwd  27508  0fallfac  27509  binomfallfaclem1  27511  binomfallfaclem2  27512  binomrisefac  27514  fallfacval4  27515  predfz  27633  bpolycl  28164  bpolysum  28165  bpolydiflem  28166  fsumkthpow  28168  bpoly4  28171  mblfinlem2  28400  iblmulc2nc  28428  fdc  28612  irrapxlem1  29134  irrapxlem2  29135  irrapxlem3  29136  pellexlem5  29145  acongrep  29294  fzmaxdif  29295  acongeq  29297  jm2.22  29315  jm2.23  29316  jm2.26lem3  29321  jm2.26  29322  jm2.27dlem2  29330  fmul01lt1lem1  29736  fmul01lt1lem2  29737  stoweidlem3  29769  stoweidlem11  29777  stoweidlem20  29786  stoweidlem26  29792  stoweidlem34  29800  stoweidlem59  29825  stirlinglem10  29849  2elfz2melfz  30173  elfzelfzlble  30180  clwwnisshclwwn  30444  erclwwlksym0  30449  erclwwlktr0  30450  erclwwlkeqlen  30453  difelfznle  30459  cshwlemma1  30460  eleclclwwlknlem2  30462  erclwwlkneqlen  30469  clwlkfclwwlk  30488  altgsumbc  30718  altgsumbcALT  30719
  Copyright terms: Public domain W3C validator