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

Theorem elfzelz 12168
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 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

Proof of Theorem elfzelz
StepHypRef Expression
1 elfzuz 12164 . 2 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ𝑀))
2 eluzelz 11529 . 2 (𝐾 ∈ (ℤ𝑀) → 𝐾 ∈ ℤ)
31, 2syl 17 1 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cfv 5790  (class class class)co 6527  cz 11210  cuz 11519  ...cfz 12152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-1st 7036  df-2nd 7037  df-neg 10120  df-z 11211  df-uz 11520  df-fz 12153
This theorem is referenced by:  fzssz  12169  elfz1eq  12178  fzsplit2  12192  fzdisj  12194  elfznn  12196  fznatpl1  12220  fzrev2i  12230  fzrev3i  12232  fznuz  12246  fzrevral  12249  fzshftral  12252  fznn0sub2  12270  elfzmlbm  12273  difelfznle  12277  predfz  12288  fzosplit  12325  fz1fzo0m1  12338  sermono  12650  seqf1olem1  12657  seqf1olem2  12658  bcval2  12909  bcval4  12911  bccmpl  12913  bcp1nk  12921  bcval5  12922  bcpasc  12925  bccl2  12927  seqcoll  13057  seqcoll2  13058  swrdval2  13218  swrd0val  13219  addlenrevswrd  13235  swrd0fv  13237  ccatswrd  13254  swrdswrd  13258  swrdswrd0  13260  swrdccatin12lem2a  13282  swrdccatin12lem2b  13283  swrdccatin2  13284  swrdccatin12  13288  spllen  13302  splfv1  13303  cshwidxm  13351  cshwidxn  13352  lswcshw  13358  2cshwcshw  13368  cshwcshid  13370  cshwcsh2id  13371  seqshft  13619  sumrblem  14235  summolem2a  14239  fsum0diaglem  14296  mptfzshft  14298  fsumrev  14299  fsumshftm  14301  fsum0diag2  14303  binomlem  14346  binom11  14349  bcxmas  14352  arisum  14377  geo2sum  14389  mertenslem1  14401  prodfn0  14411  prodrblem  14444  prodmolem2a  14449  fprodntriv  14457  fprodser  14464  fprod1p  14483  fprodrev  14492  fallfacval3  14528  fallfacfwd  14552  0fallfac  14553  binomfallfaclem1  14555  binomfallfaclem2  14556  binomrisefac  14558  fallfacval4  14559  bpolycl  14568  bpolysum  14569  bpolydiflem  14570  fsumkthpow  14572  bpoly4  14575  fzm1ndvds  14828  pwp1fsum  14898  prmdvdsfz  15201  isprm7  15204  hashdvds  15264  phiprmpw  15265  prmdiveq  15275  prmdivdiv  15276  modprminv  15288  modprminveq  15289  modprm0  15294  4sqlem11  15443  4sqlem12  15444  vdwapun  15462  prmop1  15526  prmdvdsprmo  15530  prmdvdsprmop  15531  prmgaplem1  15537  prmgaplem2  15538  prmgaplcmlem1  15539  prmgaplcmlem2  15540  prmgapprmo  15550  cshwshashlem1  15586  cshwshashlem2  15587  dfod2  17750  efgredleme  17925  efgredlemc  17927  efgredlemb  17928  gsummptshft  18105  srgbinomlem3  18311  srgbinomlem4  18312  srgbinomlem  18313  chpscmatgsummon  20411  cayhamlem1  20432  iscmet3  22817  mbfi1fseqlem4  23208  itgz  23270  itgcl  23273  ibl0  23276  iblss  23294  iblss2  23295  itgss  23301  itgeqa  23303  iblconst  23307  iblabsr  23319  iblmulc2  23320  itgsplit  23325  dvfsumlem3  23512  plyeq0lem  23687  aalioulem1  23808  cxpeq  24215  birthdaylem2  24396  wilthlem1  24511  wilthlem2  24512  wilthlem3  24513  ftalem5  24520  basellem3  24526  basellem4  24527  dvdsppwf1o  24629  dvdsflf1o  24630  musum  24634  ppiub  24646  chtublem  24653  mersenne  24669  bposlem1  24726  lgsval2lem  24749  lgsdilem2  24775  lgsqrlem2  24789  lgsqrlem4  24791  gausslemma2dlem1a  24807  gausslemma2dlem1  24808  gausslemma2dlem3  24810  gausslemma2dlem4  24811  gausslemma2dlem5a  24812  gausslemma2dlem5  24813  gausslemma2dlem6  24814  lgseisenlem1  24817  lgseisenlem2  24818  lgseisenlem3  24819  lgsquadlem1  24822  lgsquadlem2  24823  lgsquadlem3  24824  2lgslem1a1  24831  2lgslem1a  24833  2lgslem1b  24834  rpvmasumlem  24893  dchrisumlem1  24895  dchrisumlem2  24896  dchrmusum2  24900  dchrvmasumlem1  24901  dchrvmasum2lem  24902  dchrvmasum2if  24903  dchrvmasumlem3  24905  dchrvmasumiflem1  24907  dchrvmasumiflem2  24908  dchrisum0flblem1  24914  rpvmasum2  24918  dchrisum0lem1b  24921  dchrisum0lem1  24922  dchrisum0lem2a  24923  dchrisum0lem2  24924  dchrisum0lem3  24925  dchrmusumlem  24928  dchrvmasumlem  24929  logdivbnd  24962  pntpbnd1  24992  pntlemh  25005  pntlemj  25009  pntlemf  25011  ostth2lem2  25040  axlowdimlem13  25552  axlowdimlem14  25553  axlowdimlem16  25555  fargshiftfo  25932  clwwnisshclwwn  26103  erclwwlkeqlen  26106  eleclclwwlknlem2  26112  erclwwlkneqlen  26118  clwlkfclwwlk  26137  fzsplit3  28746  bcm1n  28747  ballotlemfc0  29687  ballotlemfcc  29688  ballotlemodife  29692  ballotlemimin  29700  ballotlemsgt1  29705  ballotlemsel1i  29707  ballotlemsf1o  29708  ballotlemsi  29709  ballotlemsima  29710  ballotlemfg  29720  ballotlemfrc  29721  ballotlemfrceq  29723  ballotlemfrcn0  29724  ballotlemirc  29726  ballotlem1ri  29729  erdszelem8  30240  erdszelem9  30241  cvmliftlem7  30333  supfz  30672  inffz  30673  inffzOLD  30674  bcprod  30683  fwddifnp1  31248  poimirlem1  32376  poimirlem2  32377  poimirlem7  32382  poimirlem14  32389  poimirlem15  32390  poimirlem16  32391  poimirlem17  32392  poimirlem19  32394  poimirlem20  32395  poimirlem23  32398  poimirlem24  32399  poimirlem27  32402  poimirlem28  32403  poimirlem31  32406  poimirlem32  32407  mblfinlem2  32413  iblmulc2nc  32441  fdc  32507  irrapxlem1  36200  irrapxlem2  36201  irrapxlem3  36202  pellexlem5  36211  acongrep  36361  fzmaxdif  36362  acongeq  36364  jm2.22  36376  jm2.23  36377  jm2.26lem3  36382  jm2.26  36383  jm2.27dlem2  36391  hashnzfz  37337  monoords  38248  elfzelzd  38268  fmul01lt1lem1  38448  fmul01lt1lem2  38449  sumnnodd  38494  dvnmul  38630  dvnprodlem2  38634  iblsplit  38655  iblspltprt  38662  itgspltprt  38668  stoweidlem3  38693  stoweidlem11  38701  stoweidlem20  38710  stoweidlem26  38716  stoweidlem34  38724  stoweidlem59  38749  stirlinglem10  38773  dirkertrigeqlem1  38788  dirkertrigeqlem2  38789  dirkertrigeqlem3  38790  dirkertrigeq  38791  dirkeritg  38792  fourierdlem11  38808  fourierdlem12  38809  fourierdlem15  38812  fourierdlem34  38831  fourierdlem41  38838  fourierdlem46  38842  fourierdlem48  38844  fourierdlem49  38845  fourierdlem50  38846  fourierdlem54  38850  fourierdlem63  38859  fourierdlem64  38860  fourierdlem65  38861  fourierdlem79  38875  fourierdlem102  38898  fourierdlem103  38899  fourierdlem104  38900  fourierdlem114  38910  elaa2lem  38923  etransclem4  38928  etransclem7  38931  etransclem8  38932  etransclem17  38941  etransclem18  38942  etransclem20  38944  etransclem23  38947  etransclem27  38951  etransclem31  38955  etransclem32  38956  etransclem35  38959  etransclem41  38965  etransclem46  38970  etransclem48  38972  iundjiun  39150  caratheodorylem1  39213  el1fzopredsuc  39746  iccpartgtprec  39756  iccpartiltu  39758  iccpartgt  39763  iccpartnel  39774  addlenrevpfx  40058  ccatpfx  40070  pfxccatin12lem1  40084  pfxccatin12lem2  40085  pfxccatin12  40086  2elfz2melfz  40175  elfzelfzlble  40178  crctcshlem4  41018  crctcsh1wlkn0  41019  clwwnisshclwwsn  41232  erclwwlkseqlen  41235  eleclclwwlksnlem2  41241  erclwwlksneqlen  41247  clwlksfclwwlk  41264  altgsumbc  41918  altgsumbcALT  41919  nn0sumshdiglemA  42206  nn0sumshdiglemB  42207
  Copyright terms: Public domain W3C validator