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

Theorem elfzelz 11835
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 11831 . 2  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
2 eluzelz 11202 . 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 1898   ` cfv 5605  (class class class)co 6320   ZZcz 10971   ZZ>=cuz 11193   ...cfz 11819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-cnex 9626  ax-resscn 9627
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-fv 5613  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-1st 6825  df-2nd 6826  df-neg 9894  df-z 10972  df-uz 11194  df-fz 11820
This theorem is referenced by:  fzssz  11836  elfz1eq  11845  fzsplit2  11859  fzdisj  11861  elfznn  11863  fznatpl1  11885  fzrev2i  11895  fzrev3i  11897  fznuz  11911  fzrevral  11914  fzshftral  11917  fznn0sub2  11933  elfzmlbm  11936  difelfznle  11941  predfz  11951  fzosplit  11988  fz1fzo0m1  12000  sermono  12283  seqf1olem1  12290  seqf1olem2  12291  bcval2  12528  bcval4  12530  bccmpl  12532  bcp1nk  12540  bcval5  12541  bcpasc  12544  bccl2  12546  seqcoll  12666  seqcoll2  12667  swrdval2  12819  swrd0val  12820  addlenrevswrd  12836  swrd0fv  12838  ccatswrd  12855  swrdswrd  12859  swrdswrd0  12861  swrdccatin12lem2a  12884  swrdccatin12lem2b  12885  swrdccatin2  12886  swrdccatin12  12890  spllen  12904  splfv1  12905  cshwidxm  12952  cshwidxn  12953  lswcshw  12957  2cshwcshw  12967  cshwcshid  12969  cshwcsh2id  12970  seqshft  13203  sumrblem  13832  summolem2a  13836  fsum0diaglem  13892  mptfzshft  13894  fsumrev  13895  fsumshftm  13897  fsum0diag2  13899  binomlem  13942  binom11  13945  bcxmas  13948  arisum  13973  geo2sum  13984  mertenslem1  13995  prodfn0  14005  prodrblem  14038  prodmolem2a  14043  fprodntriv  14051  fprodser  14058  fprod1p  14077  fprodrev  14086  fallfacval3  14120  fallfacfwd  14144  0fallfac  14145  binomfallfaclem1  14147  binomfallfaclem2  14148  binomrisefac  14150  fallfacval4  14151  bpolycl  14160  bpolysum  14161  bpolydiflem  14162  fsumkthpow  14164  bpoly4  14167  fzm1ndvds  14412  prmdvdsfz  14704  hashdvds  14778  phiprmpw  14779  prmdiveq  14789  prmdivdiv  14790  modprminv  14805  modprminveq  14806  modprm0  14811  4sqlem11  14954  4sqlem12  14955  vdwapun  14979  prmop1  15051  prmdvdsprmo  15055  prmdvdsprmop  15056  prmgaplem1  15062  prmgaplem2  15063  prmgaplcmlem1  15064  prmgaplcmlem2  15065  prmgaplcmlem1OLD  15067  prmgaplcmlem2OLD  15068  prmdvdsprmorOLD  15070  prmdvdsprmorpOLD  15071  prmgapprmo  15088  cshwshashlem1  15121  cshwshashlem2  15122  dfod2  17270  efgredleme  17448  efgredlemc  17450  efgredlemb  17451  gsummptshft  17624  srgbinomlem3  17830  srgbinomlem4  17831  srgbinomlem  17832  chpscmatgsummon  19924  cayhamlem1  19945  iscmet3  22318  mbfi1fseqlem4  22732  itgz  22794  itgcl  22797  ibl0  22800  iblss  22818  iblss2  22819  itgss  22825  itgeqa  22827  iblconst  22831  iblabsr  22843  iblmulc2  22844  itgsplit  22849  dvfsumlem3  23036  plyeq0lem  23220  aalioulem1  23344  cxpeq  23753  birthdaylem2  23934  wilthlem1  24049  wilthlem2  24050  wilthlem3  24051  ftalem5  24057  ftalem5OLD  24059  basellem3  24065  basellem4  24066  dvdsppwf1o  24171  dvdsflf1o  24172  musum  24176  ppiub  24188  chtublem  24195  mersenne  24211  bposlem1  24268  lgsval2lem  24290  lgsdilem2  24315  lgsqrlem2  24326  lgsqrlem4  24328  lgseisenlem1  24333  lgseisenlem2  24334  lgseisenlem3  24335  lgsquadlem1  24338  lgsquadlem2  24339  lgsquadlem3  24340  rpvmasumlem  24381  dchrisumlem1  24383  dchrisumlem2  24384  dchrmusum2  24388  dchrvmasumlem1  24389  dchrvmasum2lem  24390  dchrvmasum2if  24391  dchrvmasumlem3  24393  dchrvmasumiflem1  24395  dchrvmasumiflem2  24396  dchrisum0flblem1  24402  rpvmasum2  24406  dchrisum0lem1b  24409  dchrisum0lem1  24410  dchrisum0lem2a  24411  dchrisum0lem2  24412  dchrisum0lem3  24413  dchrmusumlem  24416  dchrvmasumlem  24417  logdivbnd  24450  pntpbnd1  24480  pntlemh  24493  pntlemj  24497  pntlemf  24499  ostth2lem2  24528  axlowdimlem13  25040  axlowdimlem14  25041  axlowdimlem16  25043  fargshiftfo  25422  clwwnisshclwwn  25593  erclwwlkeqlen  25596  eleclclwwlknlem2  25602  erclwwlkneqlen  25608  clwlkfclwwlk  25628  fzsplit3  28422  bcm1n  28423  ballotlemfc0  29375  ballotlemfcc  29376  ballotlemodife  29380  ballotlemimin  29388  ballotlemsgt1  29393  ballotlemsel1i  29395  ballotlemsf1o  29396  ballotlemsi  29397  ballotlemsima  29398  ballotlemfg  29408  ballotlemfrc  29409  ballotlemfrceq  29411  ballotlemfrcn0  29412  ballotlemirc  29414  ballotlem1ri  29417  ballotlemiminOLD  29426  ballotlemsgt1OLD  29431  ballotlemsel1iOLD  29433  ballotlemsf1oOLD  29434  ballotlemsiOLD  29435  ballotlemsimaOLD  29436  ballotlemfgOLD  29446  ballotlemfrcOLD  29447  ballotlemfrceqOLD  29449  ballotlemfrcn0OLD  29450  ballotlemircOLD  29452  ballotlem1riOLD  29455  erdszelem8  29971  erdszelem9  29972  cvmliftlem7  30064  supfz  30412  inffz  30413  bcprod  30424  fwddifnp1  30982  poimirlem1  31987  poimirlem2  31988  poimirlem7  31993  poimirlem14  32000  poimirlem15  32001  poimirlem16  32002  poimirlem17  32003  poimirlem19  32005  poimirlem20  32006  poimirlem23  32009  poimirlem24  32010  poimirlem27  32013  poimirlem28  32014  poimirlem31  32017  poimirlem32  32018  mblfinlem2  32024  iblmulc2nc  32053  fdc  32120  irrapxlem1  35712  irrapxlem2  35713  irrapxlem3  35714  pellexlem5  35723  acongrep  35876  fzmaxdif  35877  acongeq  35879  jm2.22  35896  jm2.23  35897  jm2.26lem3  35902  jm2.26  35903  jm2.27dlem2  35911  isprm7  36705  hashnzfz  36714  monoords  37589  elfzelzd  37611  fmul01lt1lem1  37748  fmul01lt1lem2  37749  sumnnodd  37796  dvnmul  37904  dvnprodlem2  37908  iblsplit  37929  iblspltprt  37936  itgspltprt  37942  stoweidlem3  37964  stoweidlem11  37972  stoweidlem20  37981  stoweidlem26  37987  stoweidlem34  37996  stoweidlem59  38021  stirlinglem10  38046  dirkertrigeqlem1  38061  dirkertrigeqlem2  38062  dirkertrigeqlem3  38063  dirkertrigeq  38064  dirkeritg  38065  fourierdlem11  38081  fourierdlem12  38082  fourierdlem15  38085  fourierdlem34  38105  fourierdlem41  38112  fourierdlem46  38117  fourierdlem48  38119  fourierdlem49  38120  fourierdlem50  38121  fourierdlem54  38125  fourierdlem63  38134  fourierdlem64  38135  fourierdlem65  38136  fourierdlem79  38150  fourierdlem102  38173  fourierdlem103  38174  fourierdlem104  38175  fourierdlem114  38185  elaa2lem  38198  elaa2lemOLD  38199  etransclem4  38204  etransclem7  38207  etransclem8  38208  etransclem17  38217  etransclem18  38218  etransclem20  38220  etransclem23  38223  etransclem27  38227  etransclem31  38231  etransclem32  38232  etransclem35  38235  etransclem41  38241  etransclem46  38246  etransclem48OLD  38248  etransclem48  38249  iundjiun  38403  caratheodorylem1  38455  el1fzopredsuc  38857  iccpartgtprec  38869  iccpartiltu  38871  iccpartgt  38876  iccpartnel  38887  addlenrevpfx  39075  ccatpfx  39087  pfxccatin12lem1  39101  pfxccatin12lem2  39102  pfxccatin12  39103  2elfz2melfz  39196  elfzelfzlble  39199  altgsumbc  40502  altgsumbcALT  40503  nn0sumshdiglemA  40799  nn0sumshdiglemB  40800
  Copyright terms: Public domain W3C validator