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

Theorem elfzle2 11017
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  |-  ( K  e.  ( M ... N )  ->  K  <_  N )

Proof of Theorem elfzle2
StepHypRef Expression
1 elfzuz3 11012 . 2  |-  ( K  e.  ( M ... N )  ->  N  e.  ( ZZ>= `  K )
)
2 eluzle 10454 . 2  |-  ( N  e.  ( ZZ>= `  K
)  ->  K  <_  N )
31, 2syl 16 1  |-  ( K  e.  ( M ... N )  ->  K  <_  N )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   class class class wbr 4172   ` cfv 5413  (class class class)co 6040    <_ cle 9077   ZZ>=cuz 10444   ...cfz 10999
This theorem is referenced by:  elfz1eq  11024  fzdisj  11034  fzp1disj  11061  uzdisj  11074  fzneuz  11083  fznuz  11084  seqf1olem1  11317  seqf1olem2  11318  bcval4  11553  bcp1nk  11563  hashf1  11661  seqcoll  11667  seqcoll2  11668  isercolllem2  12414  isercoll  12416  summolem2a  12464  fsum0diaglem  12515  mertenslem1  12616  fzm1ndvds  12856  prmind2  13045  hashdvds  13119  prmdiveq  13130  prmreclem3  13241  prmreclem5  13243  4sqlem11  13278  4sqlem12  13279  vdwlem1  13304  vdwlem3  13306  vdwlem6  13309  vdwlem9  13312  vdwlem10  13313  strlemor1  13511  mndodconglem  15134  oddvds  15140  gexdvds  15173  coe1tmmul  16624  lebnumii  18944  ovolicc2lem4  19369  voliunlem1  19397  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvfsumlem3  19865  elply2  20068  coeeq2  20114  aaliou3lem6  20218  birthdaylem2  20744  birthdaylem3  20745  wilthlem1  20804  ftalem5  20812  basellem1  20816  basellem3  20818  ppiprm  20887  chtprm  20889  logfac2  20954  lgsval2lem  21043  lgsqrlem2  21079  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgsquadlem1  21091  lgsquadlem2  21092  chebbnd1lem1  21116  dchrvmasumiflem1  21148  mulog2sumlem2  21182  pntrlog2bndlem6  21230  pntpbnd1  21233  pntpbnd2  21234  pntlemh  21246  pntlemj  21250  pntlemf  21252  eupap1  21651  bcm1n  24104  ballotlemimin  24716  ballotlemsdom  24722  ballotlemsel1i  24723  ballotlemsima  24726  ballotlemfrceq  24739  ballotlemfrcn0  24740  erdszelem8  24837  cvmliftlem2  24926  cvmliftlem7  24931  fznatpl1  25151  supfz  25152  prodmolem2a  25213  binomfallfaclem1  25306  binomfallfaclem2  25307  binomrisefac  25309  axlowdimlem16  25800  bpoly4  26009  mblfinlem  26143  irrapxlem3  26777  irrapxlem4  26778  fzmaxdif  26936  jm2.23  26957  jm2.26lem3  26962  jm2.27dlem2  26971  fmul01lt1lem1  27581  fmul01lt1lem2  27582  stoweidlem3  27619  stoweidlem17  27633  stoweidlem20  27636  stoweidlem26  27642  stoweidlem34  27650  swrd0swrd  28009
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-neg 9250  df-z 10239  df-uz 10445  df-fz 11000
  Copyright terms: Public domain W3C validator