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

Theorem elfzle1 12893
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 (𝐾 ∈ (𝑀...𝑁) → 𝑀𝐾)

Proof of Theorem elfzle1
StepHypRef Expression
1 elfzuz 12887 . 2 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ𝑀))
2 eluzle 12234 . 2 (𝐾 ∈ (ℤ𝑀) → 𝑀𝐾)
31, 2syl 17 1 (𝐾 ∈ (𝑀...𝑁) → 𝑀𝐾)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115   class class class wbr 5039  cfv 6328  (class class class)co 7130  cle 10653  cuz 12221  ...cfz 12875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-cnex 10570  ax-resscn 10571
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-id 5433  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-fv 6336  df-ov 7133  df-oprab 7134  df-mpo 7135  df-1st 7664  df-2nd 7665  df-neg 10850  df-z 11960  df-uz 12222  df-fz 12876
This theorem is referenced by:  elfz1eq  12901  fzdisj  12917  elfznn  12919  ssfzunsnext  12935  fznatpl1  12944  fznn0sub2  12997  fz0fzdiffz0  12999  difelfznle  13004  seqf1olem1  13393  seqf1olem2  13394  bcval4  13651  seqcoll  13806  seqcoll2  13807  fsum0diaglem  15110  mertenslem1  15219  fprodntriv  15275  fallfacval4  15376  divalglem6  15726  hashdvds  16089  prmdiveq  16100  4sqlem11  16268  4sqlem12  16269  dvfsumlem3  24609  birthdaylem3  25517  ppiltx  25740  ppiub  25766  lgsdilem2  25895  lgsquadlem1  25942  chtppilimlem1  26035  dchrvmasumiflem1  26063  pntrlog2bndlem5  26143  pntpbnd1  26148  pntpbnd2  26149  pntlemh  26161  pntlemj  26165  ostth2lem2  26196  axlowdimlem16  26729  fzto1st1  30751  smattr  31074  smatbl  31075  smatbr  31076  ballotlem2  31753  ballotlemsdom  31776  ballotlemsima  31780  ballotlemfrcn0  31794  ballotlem1ri  31799  breprexplemc  31910  subfacp1lem1  32433  subfacp1lem5  32438  inffz  32968  poimirlem2  34937  poimirlem6  34941  poimirlem7  34942  poimirlem8  34943  poimirlem11  34946  poimirlem15  34950  poimirlem16  34951  poimirlem17  34952  poimirlem19  34954  poimirlem20  34955  poimirlem22  34957  poimirlem24  34959  poimirlem29  34964  poimirlem31  34966  poimirlem32  34967  mblfinlem2  34973  fdc  35061  irrapxlem3  39560  acongrep  39716  fzmaxdif  39717  acongeq  39719  jm2.23  39732  jm2.26lem3  39737  jm2.27dlem2  39746  monoords  41718  fmul01lt1lem1  42017  fmul01lt1lem2  42018  sumnnodd  42063  limsupubuzlem  42145  dvnmul  42376  dvnprodlem1  42379  dvnprodlem2  42380  iblspltprt  42406  itgspltprt  42412  stoweidlem3  42436  stoweidlem11  42444  stoweidlem20  42453  stoweidlem26  42459  stoweidlem34  42467  wallispi2  42506  dirkeritg  42535  fourierdlem11  42551  fourierdlem12  42552  fourierdlem15  42555  fourierdlem41  42581  fourierdlem48  42587  fourierdlem49  42588  fourierdlem50  42589  fourierdlem52  42591  fourierdlem54  42593  fourierdlem79  42618  fourierdlem102  42641  fourierdlem103  42642  fourierdlem104  42643  fourierdlem114  42653  elaa2lem  42666  etransclem3  42670  etransclem4  42671  etransclem7  42674  etransclem10  42677  etransclem23  42690  etransclem24  42691  etransclem31  42698  etransclem32  42699  etransclem35  42702  etransclem41  42708  etransclem46  42713  caratheodorylem1  42956  iccpartgt  43735
  Copyright terms: Public domain W3C validator