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

Theorem elfzle2 11444
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 11439 . 2  |-  ( K  e.  ( M ... N )  ->  N  e.  ( ZZ>= `  K )
)
2 eluzle 10863 . 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 1757   class class class wbr 4282   ` cfv 5408  (class class class)co 6082    <_ cle 9409   ZZ>=cuz 10851   ...cfz 11426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-cnex 9328  ax-resscn 9329
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-op 3874  df-uni 4082  df-iun 4163  df-br 4283  df-opab 4341  df-mpt 4342  df-id 4625  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-fv 5416  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-1st 6568  df-2nd 6569  df-neg 9588  df-z 10637  df-uz 10852  df-fz 11427
This theorem is referenced by:  elfz1eq  11451  fzdisj  11465  fznatpl1  11497  fzp1disj  11502  uzdisj  11517  fzneuz  11527  fznuz  11528  seqf1olem1  11831  seqf1olem2  11832  bcval4  12069  bcp1nk  12079  hashf1  12196  seqcoll  12202  seqcoll2  12203  isercolllem2  13129  isercoll  13131  summolem2a  13178  fsum0diaglem  13229  mertenslem1  13329  fzm1ndvds  13570  prmind2  13759  hashdvds  13835  prmdiveq  13846  prmreclem3  13964  prmreclem5  13966  4sqlem11  14001  4sqlem12  14002  vdwlem1  14027  vdwlem3  14029  vdwlem6  14032  vdwlem9  14035  vdwlem10  14036  strlemor1  14250  mndodconglem  16026  oddvds  16032  gexdvds  16065  coe1tmmul  17630  lebnumii  20382  ovolicc2lem4  20847  voliunlem1  20875  dvfsumle  21337  dvfsumge  21338  dvfsumabs  21339  dvfsumlem3  21344  elply2  21551  coeeq2  21597  aaliou3lem6  21701  birthdaylem2  22233  birthdaylem3  22234  wilthlem1  22293  ftalem5  22301  basellem1  22305  basellem3  22307  ppiprm  22376  chtprm  22378  logfac2  22443  lgsval2lem  22532  lgsqrlem2  22568  lgseisenlem1  22575  lgseisenlem2  22576  lgseisenlem3  22577  lgsquadlem1  22580  lgsquadlem2  22581  chebbnd1lem1  22605  dchrvmasumiflem1  22637  mulog2sumlem2  22671  pntrlog2bndlem6  22719  pntpbnd1  22722  pntpbnd2  22723  pntlemh  22735  pntlemj  22739  pntlemf  22741  axlowdimlem16  23028  eupap1  23422  bcm1n  25904  ballotlemimin  26738  ballotlemsdom  26744  ballotlemsel1i  26745  ballotlemsima  26748  ballotlemfrceq  26761  ballotlemfrcn0  26762  erdszelem8  26936  cvmliftlem2  27025  cvmliftlem7  27030  supfz  27235  prodmolem2a  27296  binomrisefac  27394  bpoly4  28051  mblfinlem2  28275  irrapxlem3  29012  irrapxlem4  29013  fzmaxdif  29171  jm2.23  29192  jm2.26lem3  29197  jm2.27dlem2  29206  fmul01lt1lem1  29612  fmul01lt1lem2  29613  stoweidlem3  29646  stoweidlem17  29660  stoweidlem20  29663  stoweidlem26  29669  stoweidlem34  29677  2elfz2melfz  30050  elfzelfzlble  30057  difelfznle  30336
  Copyright terms: Public domain W3C validator