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

Theorem elfzle2 11699
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 11694 . 2  |-  ( K  e.  ( M ... N )  ->  N  e.  ( ZZ>= `  K )
)
2 eluzle 11102 . 2  |-  ( N  e.  ( ZZ>= `  K
)  ->  K  <_  N )
31, 2syl 16 1  |-  ( K  e.  ( M ... N )  ->  K  <_  N )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   class class class wbr 4437   ` cfv 5578  (class class class)co 6281    <_ cle 9632   ZZ>=cuz 11090   ...cfz 11681
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-fv 5586  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-1st 6785  df-2nd 6786  df-neg 9813  df-z 10871  df-uz 11091  df-fz 11682
This theorem is referenced by:  elfz1eq  11706  fzdisj  11721  fznatpl1  11743  fzp1disj  11747  uzdisj  11760  fzneuz  11768  fznuz  11769  elfzmlbm  11792  difelfznle  11797  nn0disj  11799  seqf1olem1  12125  seqf1olem2  12126  bcval4  12364  bcp1nk  12374  hashf1  12485  seqcoll  12491  seqcoll2  12492  isercolllem2  13467  isercoll  13469  summolem2a  13516  fsum0diaglem  13570  mertenslem1  13672  fzm1ndvds  13915  prmind2  14105  hashdvds  14182  prmdiveq  14193  prmreclem3  14313  prmreclem5  14315  4sqlem11  14350  4sqlem12  14351  vdwlem1  14376  vdwlem3  14378  vdwlem6  14381  vdwlem9  14384  vdwlem10  14385  strlemor1  14601  mndodconglem  16439  oddvds  16445  gexdvds  16478  coe1tmmul  18192  lebnumii  21339  ovolicc2lem4  21804  voliunlem1  21833  dvfsumle  22295  dvfsumge  22296  dvfsumabs  22297  dvfsumlem3  22302  elply2  22466  coeeq2  22512  aaliou3lem6  22616  birthdaylem2  23154  birthdaylem3  23155  wilthlem1  23214  ftalem5  23222  basellem1  23226  basellem3  23228  ppiprm  23297  chtprm  23299  logfac2  23364  lgsval2lem  23453  lgsqrlem2  23489  lgseisenlem1  23496  lgseisenlem2  23497  lgseisenlem3  23498  lgsquadlem1  23501  lgsquadlem2  23502  chebbnd1lem1  23526  dchrvmasumiflem1  23558  mulog2sumlem2  23592  pntrlog2bndlem6  23640  pntpbnd1  23643  pntpbnd2  23644  pntlemh  23656  pntlemj  23660  pntlemf  23662  axlowdimlem16  24132  eupap1  24848  bcm1n  27472  ballotlemimin  28317  ballotlemsdom  28323  ballotlemsel1i  28324  ballotlemsima  28327  ballotlemfrceq  28340  ballotlemfrcn0  28341  erdszelem8  28515  cvmliftlem2  28604  cvmliftlem7  28609  supfz  28980  prodmolem2a  29041  binomrisefac  29139  bpoly4  29796  mblfinlem2  30027  irrapxlem3  30735  irrapxlem4  30736  fzmaxdif  30894  jm2.23  30913  jm2.26lem3  30918  jm2.27dlem2  30927  isprm7  31168  monoords  31445  fmul01lt1lem1  31506  fmul01lt1lem2  31507  sumnnodd  31544  iblspltprt  31662  itgspltprt  31668  stoweidlem3  31674  stoweidlem17  31688  stoweidlem20  31691  stoweidlem26  31697  stoweidlem34  31705  fourierdlem11  31789  fourierdlem12  31790  fourierdlem15  31793  fourierdlem25  31803  fourierdlem41  31819  fourierdlem48  31826  fourierdlem49  31827  fourierdlem50  31828  fourierdlem52  31830  fourierdlem54  31832  fourierdlem79  31857  fourierdlem102  31880  fourierdlem114  31892  2elfz2melfz  32172  elfzelfzlble  32175
  Copyright terms: Public domain W3C validator