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

Theorem elfzelz 11692
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 11688 . 2  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
2 eluzelz 11094 . 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 1802   ` cfv 5574  (class class class)co 6277   ZZcz 10865   ZZ>=cuz 11085   ...cfz 11676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-cnex 9546  ax-resscn 9547
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-fv 5582  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-1st 6781  df-2nd 6782  df-neg 9808  df-z 10866  df-uz 11086  df-fz 11677
This theorem is referenced by:  elfz1eq  11701  fzsplit2  11714  fzdisj  11716  elfznn  11718  fznatpl1  11738  fzrev2i  11748  fzrev3i  11750  fznuz  11764  fzrevral  11766  fzshftral  11769  fznn0sub2  11784  elfzmlbm  11788  difelfznle  11792  fzosplit  11832  sermono  12113  seqf1olem1  12120  seqf1olem2  12121  bcval2  12357  bcval4  12359  bccmpl  12361  bcp1nk  12369  bcval5  12370  bcpasc  12373  bccl2  12375  seqcoll  12486  seqcoll2  12487  swrdval2  12621  swrd0val  12622  addlenrevswrd  12635  swrd0fv  12640  ccatswrd  12655  swrdswrd  12659  swrdswrd0  12661  swrdccatin12lem2a  12684  swrdccatin12lem2b  12685  swrdccatin2  12686  swrdccatin12  12690  spllen  12704  splfv1  12705  cshwidxm  12752  cshwidxn  12753  lswcshw  12757  2cshwcshw  12767  cshwcshid  12769  cshwcsh2id  12770  seqshft  12892  sumrblem  13507  summolem2a  13511  fsum0diaglem  13565  mptfzshft  13567  fsumrev  13568  fsumshftm  13570  fsum0diag2  13572  binomlem  13615  binom11  13618  bcxmas  13621  arisum  13645  geo2sum  13656  mertenslem1  13667  fzm1ndvds  13910  hashdvds  14177  phiprmpw  14178  prmdiveq  14188  prmdivdiv  14189  modprminv  14198  modprminveq  14199  modprm0  14202  4sqlem11  14345  4sqlem12  14346  vdwapun  14364  cshwshashlem1  14452  cshwshashlem2  14453  dfod2  16455  efgredleme  16630  efgredlemc  16632  efgredlemb  16633  gsummptshft  16825  srgbinomlem3  17061  srgbinomlem4  17062  srgbinomlem  17063  chpscmatgsummon  19213  cayhamlem1  19234  iscmet3  21598  mbfi1fseqlem4  21991  itgz  22053  itgcl  22056  ibl0  22059  iblss  22077  iblss2  22078  itgss  22084  itgeqa  22086  iblconst  22090  iblabsr  22102  iblmulc2  22103  itgsplit  22108  dvfsumlem3  22295  plyeq0lem  22473  aalioulem1  22593  cxpeq  22996  birthdaylem2  23147  wilthlem1  23207  wilthlem2  23208  wilthlem3  23209  ftalem5  23215  basellem3  23221  basellem4  23222  dvdsppwf1o  23327  dvdsflf1o  23328  musum  23332  ppiub  23344  chtublem  23351  mersenne  23367  bposlem1  23424  lgsval2lem  23446  lgsdilem2  23471  lgsqrlem2  23482  lgsqrlem4  23484  lgseisenlem1  23489  lgseisenlem2  23490  lgseisenlem3  23491  lgsquadlem1  23494  lgsquadlem2  23495  lgsquadlem3  23496  rpvmasumlem  23537  dchrisumlem1  23539  dchrisumlem2  23540  dchrmusum2  23544  dchrvmasumlem1  23545  dchrvmasum2lem  23546  dchrvmasum2if  23547  dchrvmasumlem3  23549  dchrvmasumiflem1  23551  dchrvmasumiflem2  23552  dchrisum0flblem1  23558  rpvmasum2  23562  dchrisum0lem1b  23565  dchrisum0lem1  23566  dchrisum0lem2a  23567  dchrisum0lem2  23568  dchrisum0lem3  23569  dchrmusumlem  23572  dchrvmasumlem  23573  logdivbnd  23606  pntpbnd1  23636  pntlemh  23649  pntlemj  23653  pntlemf  23655  ostth2lem2  23684  axlowdimlem13  24122  axlowdimlem14  24123  axlowdimlem16  24125  fargshiftfo  24503  clwwnisshclwwn  24674  erclwwlkeqlen  24677  eleclclwwlknlem2  24683  erclwwlkneqlen  24689  clwlkfclwwlk  24709  fzsplit3  27464  bcm1n  27465  ballotlemfc0  28297  ballotlemfcc  28298  ballotlemodife  28302  ballotlemimin  28310  ballotlemsgt1  28315  ballotlemsel1i  28317  ballotlemsf1o  28318  ballotlemsi  28319  ballotlemsima  28320  ballotlemfg  28330  ballotlemfrc  28331  ballotlemfrceq  28333  ballotlemfrcn0  28334  ballotlemirc  28336  ballotlem1ri  28339  erdszelem8  28508  erdszelem9  28509  cvmliftlem7  28602  supfz  28973  inffz  28974  prodfn0  28996  prodrblem  29029  prodmolem2a  29034  fprodntriv  29042  fprodser  29049  fprod1p  29065  fprodrev  29075  fallfacval3  29102  fallfacfwd  29126  0fallfac  29127  binomfallfaclem1  29129  binomfallfaclem2  29130  binomrisefac  29132  fallfacval4  29133  predfz  29251  bpolycl  29782  bpolysum  29783  bpolydiflem  29784  fsumkthpow  29786  bpoly4  29789  mblfinlem2  30020  iblmulc2nc  30048  fdc  30206  irrapxlem1  30726  irrapxlem2  30727  irrapxlem3  30728  pellexlem5  30737  acongrep  30886  fzmaxdif  30887  acongeq  30889  jm2.22  30905  jm2.23  30906  jm2.26lem3  30911  jm2.26  30912  jm2.27dlem2  30920  isprm7  31161  hashnzfz  31194  fzssz  31411  monoords  31441  fmul01lt1lem1  31502  fmul01lt1lem2  31503  sumnnodd  31540  iblsplit  31651  iblspltprt  31658  itgspltprt  31664  stoweidlem3  31670  stoweidlem11  31678  stoweidlem20  31687  stoweidlem26  31693  stoweidlem34  31701  stoweidlem59  31726  stirlinglem10  31750  dirkertrigeqlem1  31765  dirkertrigeqlem2  31766  dirkertrigeqlem3  31767  dirkertrigeq  31768  dirkeritg  31769  fourierdlem11  31785  fourierdlem12  31786  fourierdlem15  31789  fourierdlem34  31808  fourierdlem41  31815  fourierdlem46  31820  fourierdlem48  31822  fourierdlem49  31823  fourierdlem50  31824  fourierdlem54  31828  fourierdlem63  31837  fourierdlem64  31838  fourierdlem65  31839  fourierdlem79  31853  fourierdlem102  31876  fourierdlem103  31877  fourierdlem104  31878  fourierdlem114  31888  2elfz2melfz  32168  elfzelfzlble  32171  altgsumbc  32649  altgsumbcALT  32650
  Copyright terms: Public domain W3C validator