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

Theorem elfzle2 12330
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 12324 . 2 (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ𝐾))
2 eluzle 11685 . 2 (𝑁 ∈ (ℤ𝐾) → 𝐾𝑁)
31, 2syl 17 1 (𝐾 ∈ (𝑀...𝑁) → 𝐾𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988   class class class wbr 4644  cfv 5876  (class class class)co 6635  cle 10060  cuz 11672  ...cfz 12311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-1st 7153  df-2nd 7154  df-neg 10254  df-z 11363  df-uz 11673  df-fz 12312
This theorem is referenced by:  elfz1eq  12337  fzdisj  12353  ssfzunsnext  12371  fznatpl1  12380  fzp1disj  12384  uzdisj  12397  fzneuz  12405  fznuz  12406  elfzmlbm  12433  difelfznle  12437  nn0disj  12439  seqf1olem1  12823  seqf1olem2  12824  bcval4  13077  bcp1nk  13087  hashf1  13224  seqcoll  13231  seqcoll2  13232  isercolllem2  14377  isercoll  14379  summolem2a  14427  fsum0diaglem  14489  mertenslem1  14597  prodmolem2a  14645  binomrisefac  14754  bpoly4  14771  fzm1ndvds  15025  prmind2  15379  prmdvdsfz  15398  isprm7  15401  hashdvds  15461  prmdiveq  15472  prmreclem3  15603  prmreclem5  15605  4sqlem11  15640  4sqlem12  15641  vdwlem1  15666  vdwlem3  15668  vdwlem6  15671  vdwlem9  15674  vdwlem10  15675  strlemor1OLD  15950  mndodconglem  17941  oddvds  17947  gexdvds  17980  coe1tmmul  19628  lebnumii  22746  ovolicc2lem4  23269  voliunlem1  23299  dvfsumle  23765  dvfsumge  23766  dvfsumabs  23767  dvfsumlem3  23772  elply2  23933  coeeq2  23979  aaliou3lem6  24084  birthdaylem2  24660  birthdaylem3  24661  wilthlem1  24775  ftalem5  24784  basellem1  24788  basellem3  24790  ppiprm  24858  chtprm  24860  logfac2  24923  lgsval2lem  25013  lgsqrlem2  25053  lgseisenlem1  25081  lgseisenlem2  25082  lgseisenlem3  25083  lgsquadlem1  25086  lgsquadlem2  25087  2lgslem1a  25097  chebbnd1lem1  25139  dchrvmasumiflem1  25171  mulog2sumlem2  25205  pntrlog2bndlem6  25253  pntpbnd1  25256  pntpbnd2  25257  pntlemh  25269  pntlemj  25273  pntlemf  25275  axlowdimlem16  25818  crctcshwlkn0lem2  26684  crctcshlem4  26693  bcm1n  29528  psgnfzto1stlem  29824  smatrcl  29836  submateqlem1  29847  madjusmdetlem2  29868  ballotlemimin  30541  ballotlemsdom  30547  ballotlemsel1i  30548  ballotlemsima  30551  ballotlemfrceq  30564  ballotlemfrcn0  30565  fsum2dsub  30659  reprgt  30673  breprexplemc  30684  erdszelem8  31154  cvmliftlem2  31242  cvmliftlem7  31247  supfz  31588  bcprod  31599  bccolsum  31600  poimirlem2  33382  poimirlem3  33383  poimirlem4  33384  poimirlem6  33386  poimirlem7  33387  poimirlem8  33388  poimirlem12  33392  poimirlem13  33393  poimirlem14  33394  poimirlem15  33395  poimirlem16  33396  poimirlem17  33397  poimirlem19  33399  poimirlem20  33400  poimirlem21  33401  poimirlem22  33402  poimirlem23  33403  poimirlem24  33404  poimirlem26  33406  poimirlem28  33408  poimirlem29  33409  poimirlem31  33411  poimirlem32  33412  mblfinlem2  33418  irrapxlem3  37207  irrapxlem4  37208  fzmaxdif  37367  jm2.23  37382  jm2.26lem3  37387  jm2.27dlem2  37396  binomcxplemnn0  38368  monoords  39324  elfzolem1  39350  fmul01lt1lem1  39616  fmul01lt1lem2  39617  sumnnodd  39662  dvnmul  39921  dvnprodlem1  39924  dvnprodlem2  39925  iblspltprt  39952  itgspltprt  39958  stoweidlem3  39983  stoweidlem17  39997  stoweidlem20  40000  stoweidlem26  40006  stoweidlem34  40014  fourierdlem11  40098  fourierdlem12  40099  fourierdlem15  40102  fourierdlem25  40112  fourierdlem41  40128  fourierdlem48  40134  fourierdlem49  40135  fourierdlem50  40136  fourierdlem52  40138  fourierdlem54  40140  fourierdlem79  40165  fourierdlem102  40188  fourierdlem114  40200  elaa2lem  40213  etransclem23  40237  etransclem28  40242  etransclem35  40249  etransclem38  40252  iundjiun  40440  2elfz2melfz  41091  elfzelfzlble  41094  iccpartgt  41127  fmtno4prm  41252  difmodm1lt  42082
  Copyright terms: Public domain W3C validator