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

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

Proof of Theorem elfzle2
StepHypRef Expression
1 elfzuz3 12377 . 2 (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ𝐾))
2 eluzle 11738 . 2 (𝑁 ∈ (ℤ𝐾) → 𝐾𝑁)
31, 2syl 17 1 (𝐾 ∈ (𝑀...𝑁) → 𝐾𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030   class class class wbr 4685  cfv 5926  (class class class)co 6690  cle 10113  cuz 11725  ...cfz 12364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-neg 10307  df-z 11416  df-uz 11726  df-fz 12365
This theorem is referenced by:  elfz1eq  12390  fzdisj  12406  ssfzunsnext  12424  fznatpl1  12433  fzp1disj  12437  uzdisj  12451  fzneuz  12459  fznuz  12460  elfzmlbm  12488  difelfznle  12492  nn0disj  12494  seqf1olem1  12880  seqf1olem2  12881  bcval4  13134  bcp1nk  13144  hashf1  13279  seqcoll  13286  seqcoll2  13287  isercolllem2  14440  isercoll  14442  summolem2a  14490  fsum0diaglem  14552  mertenslem1  14660  prodmolem2a  14708  binomrisefac  14817  bpoly4  14834  fzm1ndvds  15091  prmind2  15445  prmdvdsfz  15464  isprm7  15467  hashdvds  15527  prmdiveq  15538  prmreclem3  15669  prmreclem5  15671  4sqlem11  15706  4sqlem12  15707  vdwlem1  15732  vdwlem3  15734  vdwlem6  15737  vdwlem9  15740  vdwlem10  15741  strlemor1OLD  16016  mndodconglem  18006  oddvds  18012  gexdvds  18045  coe1tmmul  19695  lebnumii  22812  ovolicc2lem4  23334  voliunlem1  23364  dvfsumle  23829  dvfsumge  23830  dvfsumabs  23831  dvfsumlem3  23836  elply2  23997  coeeq2  24043  aaliou3lem6  24148  birthdaylem2  24724  birthdaylem3  24725  wilthlem1  24839  ftalem5  24848  basellem1  24852  basellem3  24854  ppiprm  24922  chtprm  24924  logfac2  24987  lgsval2lem  25077  lgsqrlem2  25117  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem3  25147  lgsquadlem1  25150  lgsquadlem2  25151  2lgslem1a  25161  chebbnd1lem1  25203  dchrvmasumiflem1  25235  mulog2sumlem2  25269  pntrlog2bndlem6  25317  pntpbnd1  25320  pntpbnd2  25321  pntlemh  25333  pntlemj  25337  pntlemf  25339  axlowdimlem16  25882  crctcshwlkn0lem2  26759  crctcshlem4  26768  bcm1n  29682  psgnfzto1stlem  29978  smatrcl  29990  submateqlem1  30001  madjusmdetlem2  30022  ballotlemimin  30695  ballotlemsdom  30701  ballotlemsel1i  30702  ballotlemsima  30705  ballotlemfrceq  30718  ballotlemfrcn0  30719  fsum2dsub  30813  reprgt  30827  breprexplemc  30838  erdszelem8  31306  cvmliftlem2  31394  cvmliftlem7  31399  supfz  31739  bcprod  31750  bccolsum  31751  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem12  33551  poimirlem13  33552  poimirlem14  33553  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem23  33562  poimirlem24  33563  poimirlem26  33565  poimirlem28  33567  poimirlem29  33568  poimirlem31  33570  poimirlem32  33571  mblfinlem2  33577  irrapxlem3  37705  irrapxlem4  37706  fzmaxdif  37865  jm2.23  37880  jm2.26lem3  37885  jm2.27dlem2  37894  binomcxplemnn0  38865  monoords  39825  elfzolem1  39850  fmul01lt1lem1  40134  fmul01lt1lem2  40135  sumnnodd  40180  dvnmul  40476  dvnprodlem1  40479  dvnprodlem2  40480  iblspltprt  40507  itgspltprt  40513  stoweidlem3  40538  stoweidlem17  40552  stoweidlem20  40555  stoweidlem26  40561  stoweidlem34  40569  fourierdlem11  40653  fourierdlem12  40654  fourierdlem15  40657  fourierdlem25  40667  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem52  40693  fourierdlem54  40695  fourierdlem79  40720  fourierdlem102  40743  fourierdlem114  40755  elaa2lem  40768  etransclem23  40792  etransclem28  40797  etransclem35  40804  etransclem38  40807  iundjiun  40995  2elfz2melfz  41653  elfzelfzlble  41656  iccpartgt  41688  fmtno4prm  41812  difmodm1lt  42642
  Copyright terms: Public domain W3C validator