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

Theorem elfzle2 11571
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 11566 . 2  |-  ( K  e.  ( M ... N )  ->  N  e.  ( ZZ>= `  K )
)
2 eluzle 10983 . 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 1758   class class class wbr 4399   ` cfv 5525  (class class class)co 6199    <_ cle 9529   ZZ>=cuz 10971   ...cfz 11553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-cnex 9448  ax-resscn 9449
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-fv 5533  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-1st 6686  df-2nd 6687  df-neg 9708  df-z 10757  df-uz 10972  df-fz 11554
This theorem is referenced by:  elfz1eq  11578  fzdisj  11592  fznatpl1  11626  fzp1disj  11631  uzdisj  11647  fzneuz  11657  fznuz  11658  seqf1olem1  11961  seqf1olem2  11962  bcval4  12199  bcp1nk  12209  hashf1  12327  seqcoll  12333  seqcoll2  12334  isercolllem2  13260  isercoll  13262  summolem2a  13309  fsum0diaglem  13360  mertenslem1  13461  fzm1ndvds  13702  prmind2  13891  hashdvds  13967  prmdiveq  13978  prmreclem3  14096  prmreclem5  14098  4sqlem11  14133  4sqlem12  14134  vdwlem1  14159  vdwlem3  14161  vdwlem6  14164  vdwlem9  14167  vdwlem10  14168  strlemor1  14383  mndodconglem  16164  oddvds  16170  gexdvds  16203  coe1tmmul  17853  lebnumii  20669  ovolicc2lem4  21134  voliunlem1  21163  dvfsumle  21625  dvfsumge  21626  dvfsumabs  21627  dvfsumlem3  21632  elply2  21796  coeeq2  21842  aaliou3lem6  21946  birthdaylem2  22478  birthdaylem3  22479  wilthlem1  22538  ftalem5  22546  basellem1  22550  basellem3  22552  ppiprm  22621  chtprm  22623  logfac2  22688  lgsval2lem  22777  lgsqrlem2  22813  lgseisenlem1  22820  lgseisenlem2  22821  lgseisenlem3  22822  lgsquadlem1  22825  lgsquadlem2  22826  chebbnd1lem1  22850  dchrvmasumiflem1  22882  mulog2sumlem2  22916  pntrlog2bndlem6  22964  pntpbnd1  22967  pntpbnd2  22968  pntlemh  22980  pntlemj  22984  pntlemf  22986  axlowdimlem16  23354  eupap1  23748  bcm1n  26223  ballotlemimin  27031  ballotlemsdom  27037  ballotlemsel1i  27038  ballotlemsima  27041  ballotlemfrceq  27054  ballotlemfrcn0  27055  erdszelem8  27229  cvmliftlem2  27318  cvmliftlem7  27323  supfz  27529  prodmolem2a  27590  binomrisefac  27688  bpoly4  28345  mblfinlem2  28576  irrapxlem3  29312  irrapxlem4  29313  fzmaxdif  29471  jm2.23  29492  jm2.26lem3  29497  jm2.27dlem2  29506  fmul01lt1lem1  29912  fmul01lt1lem2  29913  stoweidlem3  29945  stoweidlem17  29959  stoweidlem20  29962  stoweidlem26  29968  stoweidlem34  29976  2elfz2melfz  30349  elfzelfzlble  30356  difelfznle  30635  nn0disj  30885
  Copyright terms: Public domain W3C validator