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

Theorem elfzle2 11063
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 11058 . 2  |-  ( K  e.  ( M ... N )  ->  N  e.  ( ZZ>= `  K )
)
2 eluzle 10500 . 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 1726   class class class wbr 4214   ` cfv 5456  (class class class)co 6083    <_ cle 9123   ZZ>=cuz 10490   ...cfz 11045
This theorem is referenced by:  elfz1eq  11070  fzdisj  11080  fzp1disj  11107  uzdisj  11121  fzneuz  11130  fznuz  11131  seqf1olem1  11364  seqf1olem2  11365  bcval4  11600  bcp1nk  11610  hashf1  11708  seqcoll  11714  seqcoll2  11715  isercolllem2  12461  isercoll  12463  summolem2a  12511  fsum0diaglem  12562  mertenslem1  12663  fzm1ndvds  12903  prmind2  13092  hashdvds  13166  prmdiveq  13177  prmreclem3  13288  prmreclem5  13290  4sqlem11  13325  4sqlem12  13326  vdwlem1  13351  vdwlem3  13353  vdwlem6  13356  vdwlem9  13359  vdwlem10  13360  strlemor1  13558  mndodconglem  15181  oddvds  15187  gexdvds  15220  coe1tmmul  16671  lebnumii  18993  ovolicc2lem4  19418  voliunlem1  19446  dvfsumle  19907  dvfsumge  19908  dvfsumabs  19909  dvfsumlem3  19914  elply2  20117  coeeq2  20163  aaliou3lem6  20267  birthdaylem2  20793  birthdaylem3  20794  wilthlem1  20853  ftalem5  20861  basellem1  20865  basellem3  20867  ppiprm  20936  chtprm  20938  logfac2  21003  lgsval2lem  21092  lgsqrlem2  21128  lgseisenlem1  21135  lgseisenlem2  21136  lgseisenlem3  21137  lgsquadlem1  21140  lgsquadlem2  21141  chebbnd1lem1  21165  dchrvmasumiflem1  21197  mulog2sumlem2  21231  pntrlog2bndlem6  21279  pntpbnd1  21282  pntpbnd2  21283  pntlemh  21295  pntlemj  21299  pntlemf  21301  eupap1  21700  bcm1n  24153  ballotlemimin  24765  ballotlemsdom  24771  ballotlemsel1i  24772  ballotlemsima  24775  ballotlemfrceq  24788  ballotlemfrcn0  24789  erdszelem8  24886  cvmliftlem2  24975  cvmliftlem7  24980  fznatpl1  25200  supfz  25201  prodmolem2a  25262  binomrisefac  25360  axlowdimlem16  25898  bpoly4  26107  mblfinlem2  26246  irrapxlem3  26889  irrapxlem4  26890  fzmaxdif  27048  jm2.23  27069  jm2.26lem3  27074  jm2.27dlem2  27083  fmul01lt1lem1  27692  fmul01lt1lem2  27693  stoweidlem3  27730  stoweidlem17  27744  stoweidlem20  27747  stoweidlem26  27753  stoweidlem34  27761  2elfz2melfz  28119  swrd0swrd  28199  2cshw2lem2  28255
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-cnex 9048  ax-resscn 9049
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-iun 4097  df-br 4215  df-opab 4269  df-mpt 4270  df-id 4500  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-fv 5464  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-1st 6351  df-2nd 6352  df-neg 9296  df-z 10285  df-uz 10491  df-fz 11046
  Copyright terms: Public domain W3C validator