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

Theorem elfzle2 13454
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 13447 . 2 (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ𝐾))
2 eluzle 12784 . 2 (𝑁 ∈ (ℤ𝐾) → 𝐾𝑁)
31, 2syl 17 1 (𝐾 ∈ (𝑀...𝑁) → 𝐾𝑁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107   class class class wbr 5109  cfv 6500  (class class class)co 7361  cle 11198  cuz 12771  ...cfz 13433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pr 5388  ax-un 7676  ax-cnex 11115  ax-resscn 11116
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7925  df-2nd 7926  df-neg 11396  df-z 12508  df-uz 12772  df-fz 13434
This theorem is referenced by:  elfz1eq  13461  fzdisj  13477  ssfzunsnext  13495  fznatpl1  13504  fzp1disj  13509  uzdisj  13523  fzneuz  13531  fznuz  13532  elfzmlbm  13560  difelfznle  13564  nn0disj  13566  seqf1olem1  13956  seqf1olem2  13957  bcval4  14216  bcp1nk  14226  hashf1  14365  seqcoll  14372  seqcoll2  14373  isercolllem2  15559  isercoll  15561  summolem2a  15608  fsum0diaglem  15669  mertenslem1  15777  prodmolem2a  15825  binomrisefac  15933  bpoly4  15950  fzm1ndvds  16212  prmind2  16569  prmdvdsfz  16589  isprm7  16592  hashdvds  16655  prmdiveq  16666  prmreclem3  16798  prmreclem5  16800  4sqlem11  16835  4sqlem12  16836  vdwlem1  16861  vdwlem3  16863  vdwlem6  16866  vdwlem9  16869  vdwlem10  16870  mndodconglem  19331  oddvds  19337  gexdvds  19374  coe1tmmul  21671  lebnumii  24352  ovolicc2lem4  24907  voliunlem1  24937  dvfsumle  25408  dvfsumge  25409  dvfsumabs  25410  dvfsumlem3  25415  elply2  25580  coeeq2  25626  aaliou3lem6  25731  birthdaylem2  26325  birthdaylem3  26326  wilthlem1  26440  ftalem5  26449  basellem1  26453  basellem3  26455  ppiprm  26523  chtprm  26525  logfac2  26588  lgsval2lem  26678  lgsqrlem2  26718  lgseisenlem1  26746  lgseisenlem2  26747  lgseisenlem3  26748  lgsquadlem1  26751  lgsquadlem2  26752  2lgslem1a  26762  chebbnd1lem1  26840  dchrvmasumiflem1  26872  mulog2sumlem2  26906  pntrlog2bndlem6  26954  pntpbnd1  26957  pntpbnd2  26958  pntlemh  26970  pntlemj  26974  pntlemf  26976  axlowdimlem16  27955  crctcshwlkn0lem2  28805  crctcshlem4  28814  bcm1n  31752  psgnfzto1stlem  32005  cycpmco2lem6  32036  cycpmco2lem7  32037  smatrcl  32441  submateqlem1  32452  madjusmdetlem2  32473  ballotlemimin  33169  ballotlemsdom  33175  ballotlemsel1i  33176  ballotlemsima  33179  ballotlemfrceq  33192  ballotlemfrcn0  33193  fsum2dsub  33284  reprgt  33298  breprexplemc  33309  erdszelem8  33856  cvmliftlem2  33944  cvmliftlem7  33949  supfz  34364  bcprod  34374  bccolsum  34375  poimirlem2  36130  poimirlem3  36131  poimirlem4  36132  poimirlem6  36134  poimirlem7  36135  poimirlem8  36136  poimirlem12  36140  poimirlem13  36141  poimirlem14  36142  poimirlem15  36143  poimirlem16  36144  poimirlem17  36145  poimirlem19  36147  poimirlem20  36148  poimirlem21  36149  poimirlem22  36150  poimirlem23  36151  poimirlem24  36152  poimirlem26  36154  poimirlem28  36156  poimirlem29  36157  poimirlem31  36159  poimirlem32  36160  mblfinlem2  36166  aks4d1p5  40587  aks4d1p6  40588  aks4d1p8  40594  sticksstones6  40609  sticksstones7  40610  sticksstones10  40613  sticksstones12a  40615  sticksstones12  40616  metakunt1  40627  metakunt7  40633  metakunt15  40641  metakunt16  40642  metakunt22  40648  metakunt28  40654  metakunt30  40656  irrapxlem3  41194  irrapxlem4  41195  fzmaxdif  41352  jm2.23  41367  jm2.26lem3  41372  jm2.27dlem2  41381  binomcxplemnn0  42721  monoords  43622  elfzolem1  43646  fmul01lt1lem1  43915  fmul01lt1lem2  43916  sumnnodd  43961  dvnmul  44274  dvnprodlem1  44277  dvnprodlem2  44278  iblspltprt  44304  itgspltprt  44310  stoweidlem3  44334  stoweidlem17  44348  stoweidlem20  44351  stoweidlem26  44357  stoweidlem34  44365  fourierdlem11  44449  fourierdlem12  44450  fourierdlem15  44453  fourierdlem25  44463  fourierdlem41  44479  fourierdlem48  44485  fourierdlem49  44486  fourierdlem50  44487  fourierdlem52  44489  fourierdlem54  44491  fourierdlem79  44516  fourierdlem102  44539  fourierdlem114  44551  elaa2lem  44564  etransclem23  44588  etransclem28  44593  etransclem35  44600  etransclem38  44603  iundjiun  44791  2elfz2melfz  45640  elfzelfzlble  45643  iccpartgt  45709  fmtno4prm  45857  difmodm1lt  46698
  Copyright terms: Public domain W3C validator