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

Theorem elfzle2 12901
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 12895 . 2 (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ𝐾))
2 eluzle 12245 . 2 (𝑁 ∈ (ℤ𝐾) → 𝐾𝑁)
31, 2syl 17 1 (𝐾 ∈ (𝑀...𝑁) → 𝐾𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105   class class class wbr 5058  cfv 6349  (class class class)co 7145  cle 10665  cuz 12232  ...cfz 12882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-fv 6357  df-ov 7148  df-oprab 7149  df-mpo 7150  df-1st 7680  df-2nd 7681  df-neg 10862  df-z 11971  df-uz 12233  df-fz 12883
This theorem is referenced by:  elfz1eq  12908  fzdisj  12924  ssfzunsnext  12942  fznatpl1  12951  fzp1disj  12956  uzdisj  12970  fzneuz  12978  fznuz  12979  elfzmlbm  13007  difelfznle  13011  nn0disj  13013  seqf1olem1  13399  seqf1olem2  13400  bcval4  13657  bcp1nk  13667  hashf1  13805  seqcoll  13812  seqcoll2  13813  isercolllem2  15012  isercoll  15014  summolem2a  15062  fsum0diaglem  15121  mertenslem1  15230  prodmolem2a  15278  binomrisefac  15386  bpoly4  15403  fzm1ndvds  15662  prmind2  16019  prmdvdsfz  16039  isprm7  16042  hashdvds  16102  prmdiveq  16113  prmreclem3  16244  prmreclem5  16246  4sqlem11  16281  4sqlem12  16282  vdwlem1  16307  vdwlem3  16309  vdwlem6  16312  vdwlem9  16315  vdwlem10  16316  mndodconglem  18600  oddvds  18606  gexdvds  18640  coe1tmmul  20375  lebnumii  23499  ovolicc2lem4  24050  voliunlem1  24080  dvfsumle  24547  dvfsumge  24548  dvfsumabs  24549  dvfsumlem3  24554  elply2  24715  coeeq2  24761  aaliou3lem6  24866  birthdaylem2  25458  birthdaylem3  25459  wilthlem1  25573  ftalem5  25582  basellem1  25586  basellem3  25588  ppiprm  25656  chtprm  25658  logfac2  25721  lgsval2lem  25811  lgsqrlem2  25851  lgseisenlem1  25879  lgseisenlem2  25880  lgseisenlem3  25881  lgsquadlem1  25884  lgsquadlem2  25885  2lgslem1a  25895  chebbnd1lem1  25973  dchrvmasumiflem1  26005  mulog2sumlem2  26039  pntrlog2bndlem6  26087  pntpbnd1  26090  pntpbnd2  26091  pntlemh  26103  pntlemj  26107  pntlemf  26109  axlowdimlem16  26671  crctcshwlkn0lem2  27517  crctcshlem4  27526  bcm1n  30445  psgnfzto1stlem  30670  cycpmco2lem6  30701  cycpmco2lem7  30702  smatrcl  30961  submateqlem1  30972  madjusmdetlem2  30993  ballotlemimin  31663  ballotlemsdom  31669  ballotlemsel1i  31670  ballotlemsima  31673  ballotlemfrceq  31686  ballotlemfrcn0  31687  fsum2dsub  31778  reprgt  31792  breprexplemc  31803  erdszelem8  32343  cvmliftlem2  32431  cvmliftlem7  32436  supfz  32858  bcprod  32868  bccolsum  32869  poimirlem2  34776  poimirlem3  34777  poimirlem4  34778  poimirlem6  34780  poimirlem7  34781  poimirlem8  34782  poimirlem12  34786  poimirlem13  34787  poimirlem14  34788  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem21  34795  poimirlem22  34796  poimirlem23  34797  poimirlem24  34798  poimirlem26  34800  poimirlem28  34802  poimirlem29  34803  poimirlem31  34805  poimirlem32  34806  mblfinlem2  34812  irrapxlem3  39301  irrapxlem4  39302  fzmaxdif  39458  jm2.23  39473  jm2.26lem3  39478  jm2.27dlem2  39487  binomcxplemnn0  40561  monoords  41444  elfzolem1  41469  fmul01lt1lem1  41745  fmul01lt1lem2  41746  sumnnodd  41791  dvnmul  42108  dvnprodlem1  42111  dvnprodlem2  42112  iblspltprt  42138  itgspltprt  42144  stoweidlem3  42169  stoweidlem17  42183  stoweidlem20  42186  stoweidlem26  42192  stoweidlem34  42200  fourierdlem11  42284  fourierdlem12  42285  fourierdlem15  42288  fourierdlem25  42298  fourierdlem41  42314  fourierdlem48  42320  fourierdlem49  42321  fourierdlem50  42322  fourierdlem52  42324  fourierdlem54  42326  fourierdlem79  42351  fourierdlem102  42374  fourierdlem114  42386  elaa2lem  42399  etransclem23  42423  etransclem28  42428  etransclem35  42435  etransclem38  42438  iundjiun  42623  2elfz2melfz  43399  elfzelfzlble  43402  iccpartgt  43434  fmtno4prm  43584  difmodm1lt  44480
  Copyright terms: Public domain W3C validator