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

Theorem elfzle2 12168
Description: A member of a finite set of sequential integer is less than or equal to the upper bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
elfzle2 (𝐾 ∈ (𝑀...𝑁) → 𝐾𝑁)

Proof of Theorem elfzle2
StepHypRef Expression
1 elfzuz3 12162 . 2 (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ𝐾))
2 eluzle 11529 . 2 (𝑁 ∈ (ℤ𝐾) → 𝐾𝑁)
31, 2syl 17 1 (𝐾 ∈ (𝑀...𝑁) → 𝐾𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976   class class class wbr 4574  cfv 5787  (class class class)co 6524  cle 9928  cuz 11516  ...cfz 12149
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 2032  ax-13 2229  ax-ext 2586  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-cnex 9845  ax-resscn 9846
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 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-id 4940  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-fv 5795  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-1st 7033  df-2nd 7034  df-neg 10117  df-z 11208  df-uz 11517  df-fz 12150
This theorem is referenced by:  elfz1eq  12175  fzdisj  12191  fznatpl1  12217  fzp1disj  12221  uzdisj  12234  fzneuz  12242  fznuz  12243  elfzmlbm  12270  difelfznle  12274  nn0disj  12276  seqf1olem1  12654  seqf1olem2  12655  bcval4  12908  bcp1nk  12918  hashf1  13047  seqcoll  13054  seqcoll2  13055  isercolllem2  14187  isercoll  14189  summolem2a  14236  fsum0diaglem  14293  mertenslem1  14398  prodmolem2a  14446  binomrisefac  14555  bpoly4  14572  fzm1ndvds  14825  prmind2  15179  prmdvdsfz  15198  isprm7  15201  hashdvds  15261  prmdiveq  15272  prmreclem3  15403  prmreclem5  15405  4sqlem11  15440  4sqlem12  15441  vdwlem1  15466  vdwlem3  15468  vdwlem6  15471  vdwlem9  15474  vdwlem10  15475  strlemor1  15739  mndodconglem  17726  oddvds  17732  gexdvds  17765  coe1tmmul  19411  lebnumii  22501  ovolicc2lem4  23009  voliunlem1  23039  dvfsumle  23502  dvfsumge  23503  dvfsumabs  23504  dvfsumlem3  23509  elply2  23670  coeeq2  23716  aaliou3lem6  23821  birthdaylem2  24393  birthdaylem3  24394  wilthlem1  24508  ftalem5  24517  basellem1  24521  basellem3  24523  ppiprm  24591  chtprm  24593  logfac2  24656  lgsval2lem  24746  lgsqrlem2  24786  lgseisenlem1  24814  lgseisenlem2  24815  lgseisenlem3  24816  lgsquadlem1  24819  lgsquadlem2  24820  2lgslem1a  24830  chebbnd1lem1  24872  dchrvmasumiflem1  24904  mulog2sumlem2  24938  pntrlog2bndlem6  24986  pntpbnd1  24989  pntpbnd2  24990  pntlemh  25002  pntlemj  25006  pntlemf  25008  axlowdimlem16  25552  eupap1  26266  bcm1n  28744  psgnfzto1stlem  28984  smatrcl  28993  submateqlem1  29004  madjusmdetlem2  29025  ballotlemimin  29697  ballotlemsdom  29703  ballotlemsel1i  29704  ballotlemsima  29707  ballotlemfrceq  29720  ballotlemfrcn0  29721  erdszelem8  30237  cvmliftlem2  30325  cvmliftlem7  30330  supfz  30669  bcprod  30680  bccolsum  30681  poimirlem2  32381  poimirlem3  32382  poimirlem4  32383  poimirlem6  32385  poimirlem7  32386  poimirlem8  32387  poimirlem12  32391  poimirlem13  32392  poimirlem14  32393  poimirlem15  32394  poimirlem16  32395  poimirlem17  32396  poimirlem19  32398  poimirlem20  32399  poimirlem21  32400  poimirlem22  32401  poimirlem23  32402  poimirlem24  32403  poimirlem26  32405  poimirlem28  32407  poimirlem29  32408  poimirlem31  32410  poimirlem32  32411  mblfinlem2  32417  irrapxlem3  36206  irrapxlem4  36207  fzmaxdif  36366  jm2.23  36381  jm2.26lem3  36386  jm2.27dlem2  36395  binomcxplemnn0  37370  monoords  38252  elfzolem1  38279  fmul01lt1lem1  38452  fmul01lt1lem2  38453  sumnnodd  38498  dvnmul  38634  dvnprodlem1  38637  dvnprodlem2  38638  iblspltprt  38666  itgspltprt  38672  stoweidlem3  38697  stoweidlem17  38711  stoweidlem20  38714  stoweidlem26  38720  stoweidlem34  38728  fourierdlem11  38812  fourierdlem12  38813  fourierdlem15  38816  fourierdlem25  38826  fourierdlem41  38842  fourierdlem48  38848  fourierdlem49  38849  fourierdlem50  38850  fourierdlem52  38852  fourierdlem54  38854  fourierdlem79  38879  fourierdlem102  38902  fourierdlem114  38914  elaa2lem  38927  etransclem23  38951  etransclem28  38956  etransclem35  38963  etransclem38  38966  iundjiun  39154  iccpartgt  39767  fmtno4prm  39827  2elfz2melfz  40179  elfzelfzlble  40182  crctcsh1wlkn0lem2  41013  crctcshlem4  41022  difmodm1lt  42110
  Copyright terms: Public domain W3C validator