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

Theorem elfzle1 11678
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 11673 . 2  |-  ( K  e.  ( M ... N )  ->  K  e.  ( ZZ>= `  M )
)
2 eluzle 11083 . 2  |-  ( K  e.  ( ZZ>= `  M
)  ->  M  <_  K )
31, 2syl 16 1  |-  ( K  e.  ( M ... N )  ->  M  <_  K )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1762   class class class wbr 4440   ` cfv 5579  (class class class)co 6275    <_ cle 9618   ZZ>=cuz 11071   ...cfz 11661
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 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-cnex 9537  ax-resscn 9538
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-fv 5587  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-1st 6774  df-2nd 6775  df-neg 9797  df-z 10854  df-uz 11072  df-fz 11662
This theorem is referenced by:  elfz1eq  11686  fzdisj  11701  elfznn  11703  fznatpl1  11723  fznn0sub2  11768  fz0fzdiffz0  11770  difelfznle  11775  seqf1olem1  12102  seqf1olem2  12103  bcval4  12340  seqcoll  12465  seqcoll2  12466  fsum0diaglem  13540  mertenslem1  13645  divalglem6  13904  hashdvds  14153  prmdiveq  14164  4sqlem11  14321  4sqlem12  14322  dvfsumlem3  22157  birthdaylem3  23004  ppiltx  23172  ppiub  23200  lgsdilem2  23327  lgsquadlem1  23350  chtppilimlem1  23379  dchrvmasumiflem1  23407  pntrlog2bndlem5  23487  pntpbnd1  23492  pntpbnd2  23493  pntlemh  23505  pntlemj  23509  ostth2lem2  23540  axlowdimlem16  23929  ballotlem2  27917  ballotlemsdom  27940  ballotlemsima  27944  ballotlemfrcn0  27958  ballotlem1ri  27963  subfacp1lem1  28113  subfacp1lem5  28118  inffz  28433  fprodntriv  28501  fallfacval4  28592  mblfinlem2  29480  fdc  29692  irrapxlem3  30215  acongrep  30373  fzmaxdif  30374  acongeq  30376  jm2.23  30395  jm2.26lem3  30400  jm2.27dlem2  30409  monoords  30892  fmul01lt1lem1  30953  fmul01lt1lem2  30954  sumnnodd  30991  iblspltprt  31110  itgspltprt  31116  stoweidlem3  31122  stoweidlem11  31130  stoweidlem20  31139  stoweidlem26  31145  stoweidlem34  31153  wallispi2  31192  dirkeritg  31221  fourierdlem11  31237  fourierdlem12  31238  fourierdlem15  31241  fourierdlem41  31267  fourierdlem48  31274  fourierdlem49  31275  fourierdlem50  31276  fourierdlem52  31278  fourierdlem54  31280  fourierdlem79  31305  fourierdlem102  31328  fourierdlem103  31329  fourierdlem104  31330  fourierdlem114  31340
  Copyright terms: Public domain W3C validator