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

Theorem elfzle1 11743
Description: A member of a finite set of sequential integer is greater than or equal to the lower bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
elfzle1  |-  ( K  e.  ( M ... N )  ->  M  <_  K )

Proof of Theorem elfzle1
StepHypRef Expression
1 elfzuz 11738 . 2  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
2 eluzle 11139 . 2  |-  ( K  e.  ( ZZ>= `  M
)  ->  M  <_  K )
31, 2syl 17 1  |-  ( K  e.  ( M ... N )  ->  M  <_  K )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   class class class wbr 4395   ` cfv 5569  (class class class)co 6278    <_ cle 9659   ZZ>=cuz 11127   ...cfz 11726
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-cnex 9578  ax-resscn 9579
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-fv 5577  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-1st 6784  df-2nd 6785  df-neg 9844  df-z 10906  df-uz 11128  df-fz 11727
This theorem is referenced by:  elfz1eq  11751  fzdisj  11766  elfznn  11768  fznatpl1  11789  fznn0sub2  11836  fz0fzdiffz0  11838  difelfznle  11844  seqf1olem1  12190  seqf1olem2  12191  bcval4  12429  seqcoll  12561  seqcoll2  12562  fsum0diaglem  13742  mertenslem1  13845  fprodntriv  13901  fallfacval4  13988  divalglem6  14265  hashdvds  14514  prmdiveq  14525  4sqlem11  14682  4sqlem12  14683  dvfsumlem3  22721  birthdaylem3  23609  ppiltx  23832  ppiub  23860  lgsdilem2  23987  lgsquadlem1  24010  chtppilimlem1  24039  dchrvmasumiflem1  24067  pntrlog2bndlem5  24147  pntpbnd1  24152  pntpbnd2  24153  pntlemh  24165  pntlemj  24169  ostth2lem2  24200  axlowdimlem16  24677  ballotlem2  28933  ballotlemsdom  28956  ballotlemsima  28960  ballotlemfrcn0  28974  ballotlem1ri  28979  subfacp1lem1  29476  subfacp1lem5  29481  inffz  29936  mblfinlem2  31424  fdc  31520  irrapxlem3  35121  acongrep  35279  fzmaxdif  35280  acongeq  35282  jm2.23  35300  jm2.26lem3  35305  jm2.27dlem2  35314  monoords  36865  fmul01lt1lem1  36946  fmul01lt1lem2  36947  sumnnodd  37004  dvnmul  37108  dvnprodlem1  37111  dvnprodlem2  37112  iblspltprt  37140  itgspltprt  37146  stoweidlem3  37153  stoweidlem11  37161  stoweidlem20  37170  stoweidlem26  37176  stoweidlem34  37184  wallispi2  37223  dirkeritg  37252  fourierdlem11  37268  fourierdlem12  37269  fourierdlem15  37272  fourierdlem41  37298  fourierdlem48  37305  fourierdlem49  37306  fourierdlem50  37307  fourierdlem52  37309  fourierdlem54  37311  fourierdlem79  37336  fourierdlem102  37359  fourierdlem103  37360  fourierdlem104  37361  fourierdlem114  37371  elaa2lem  37384  etransclem3  37388  etransclem4  37389  etransclem7  37392  etransclem10  37395  etransclem23  37408  etransclem24  37409  etransclem31  37416  etransclem32  37417  etransclem35  37420  etransclem41  37426  etransclem46  37431  iccpartgt  37694
  Copyright terms: Public domain W3C validator