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

Theorem elfzle2 10847
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 10842 . 2  |-  ( K  e.  ( M ... N )  ->  N  e.  ( ZZ>= `  K )
)
2 eluzle 10287 . 2  |-  ( N  e.  ( ZZ>= `  K
)  ->  K  <_  N )
31, 2syl 15 1  |-  ( K  e.  ( M ... N )  ->  K  <_  N )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1701   class class class wbr 4060   ` cfv 5292  (class class class)co 5900    <_ cle 8913   ZZ>=cuz 10277   ...cfz 10829
This theorem is referenced by:  elfz1eq  10854  fzdisj  10864  fzp1disj  10890  uzdisj  10903  fzneuz  10910  fznuz  10911  seqf1olem1  11132  seqf1olem2  11133  bcval4  11367  bcp1nk  11376  hashf1  11442  seqcoll  11448  seqcoll2  11449  isercolllem2  12186  isercoll  12188  summolem2a  12235  fsum0diaglem  12286  mertenslem1  12387  fzm1ndvds  12627  prmind2  12816  hashdvds  12890  prmdiveq  12901  prmreclem3  13012  prmreclem5  13014  4sqlem11  13049  4sqlem12  13050  vdwlem1  13075  vdwlem3  13077  vdwlem6  13080  vdwlem9  13083  vdwlem10  13084  strlemor1  13282  mndodconglem  14905  oddvds  14911  gexdvds  14944  coe1tmmul  16402  lebnumii  18517  ovolicc2lem4  18932  voliunlem1  18960  dvfsumle  19421  dvfsumge  19422  dvfsumabs  19423  dvfsumlem3  19428  elply2  19631  coeeq2  19677  aaliou3lem6  19781  birthdaylem2  20300  birthdaylem3  20301  wilthlem1  20359  ftalem5  20367  basellem1  20371  basellem3  20373  ppiprm  20442  chtprm  20444  logfac2  20509  lgsval2lem  20598  lgsqrlem2  20634  lgseisenlem1  20641  lgseisenlem2  20642  lgseisenlem3  20643  lgsquadlem1  20646  lgsquadlem2  20647  chebbnd1lem1  20671  dchrvmasumiflem1  20703  mulog2sumlem2  20737  pntrlog2bndlem6  20785  pntpbnd1  20788  pntpbnd2  20789  pntlemh  20801  pntlemj  20805  pntlemf  20807  bcm1n  23298  ballotlemimin  23937  ballotlemsdom  23943  ballotlemsel1i  23944  ballotlemsima  23947  ballotlemfrceq  23960  ballotlemfrcn0  23961  erdszelem8  24013  cvmliftlem2  24101  cvmliftlem7  24106  eupap1  24184  fznatpl1  24379  supfz  24380  prodmolem2a  24437  axlowdimlem16  24971  bpoly4  25180  irrapxlem3  26057  irrapxlem4  26058  fzmaxdif  26216  jm2.23  26237  jm2.26lem3  26242  jm2.27dlem2  26251  fmul01lt1lem1  26862  fmul01lt1lem2  26863  stoweidlem3  26900  stoweidlem17  26914  stoweidlem20  26917  stoweidlem26  26923  stoweidlem34  26931
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-cnex 8838  ax-resscn 8839
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-fv 5300  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-1st 6164  df-2nd 6165  df-neg 9085  df-z 10072  df-uz 10278  df-fz 10830
  Copyright terms: Public domain W3C validator