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

Theorem elfzle2 11801
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  |-  ( K  e.  ( M ... N )  ->  K  <_  N )

Proof of Theorem elfzle2
StepHypRef Expression
1 elfzuz3 11795 . 2  |-  ( K  e.  ( M ... N )  ->  N  e.  ( ZZ>= `  K )
)
2 eluzle 11171 . 2  |-  ( N  e.  ( ZZ>= `  K
)  ->  K  <_  N )
31, 2syl 17 1  |-  ( K  e.  ( M ... N )  ->  K  <_  N )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   class class class wbr 4426   ` cfv 5601  (class class class)co 6305    <_ cle 9675   ZZ>=cuz 11159   ...cfz 11782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-cnex 9594  ax-resscn 9595
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-1st 6807  df-2nd 6808  df-neg 9862  df-z 10938  df-uz 11160  df-fz 11783
This theorem is referenced by:  elfz1eq  11808  fzdisj  11824  fznatpl1  11848  fzp1disj  11852  uzdisj  11865  fzneuz  11873  fznuz  11874  elfzmlbm  11898  difelfznle  11903  nn0disj  11905  seqf1olem1  12249  seqf1olem2  12250  bcval4  12489  bcp1nk  12499  hashf1  12615  seqcoll  12621  seqcoll2  12622  isercolllem2  13707  isercoll  13709  summolem2a  13759  fsum0diaglem  13815  mertenslem1  13918  prodmolem2a  13966  binomrisefac  14073  bpoly4  14090  fzm1ndvds  14335  prmind2  14606  prmdvdsfz  14620  hashdvds  14692  prmdiveq  14703  prmreclem3  14825  prmreclem5  14827  4sqlem11  14862  4sqlem12  14863  vdwlem1  14894  vdwlem3  14896  vdwlem6  14899  vdwlem9  14902  vdwlem10  14903  strlemor1  15179  mndodconglem  17132  oddvds  17138  gexdvds  17171  coe1tmmul  18805  lebnumii  21890  ovolicc2lem4  22351  voliunlem1  22380  dvfsumle  22850  dvfsumge  22851  dvfsumabs  22852  dvfsumlem3  22857  elply2  23018  coeeq2  23064  aaliou3lem6  23169  birthdaylem2  23743  birthdaylem3  23744  wilthlem1  23858  ftalem5  23866  basellem1  23870  basellem3  23872  ppiprm  23941  chtprm  23943  logfac2  24008  lgsval2lem  24097  lgsqrlem2  24133  lgseisenlem1  24140  lgseisenlem2  24141  lgseisenlem3  24142  lgsquadlem1  24145  lgsquadlem2  24146  chebbnd1lem1  24170  dchrvmasumiflem1  24202  mulog2sumlem2  24236  pntrlog2bndlem6  24284  pntpbnd1  24287  pntpbnd2  24288  pntlemh  24300  pntlemj  24304  pntlemf  24306  axlowdimlem16  24833  eupap1  25549  bcm1n  28207  psgnfzto1stlem  28452  smatrcl  28461  submateqlem1  28472  madjusmdetlem2  28493  ballotlemimin  29164  ballotlemsdom  29170  ballotlemsel1i  29171  ballotlemsima  29174  ballotlemfrceq  29187  ballotlemfrcn0  29188  erdszelem8  29709  cvmliftlem2  29797  cvmliftlem7  29802  supfz  30149  bcprod  30161  bccolsum  30162  poimirlem2  31646  poimirlem3  31647  poimirlem4  31648  poimirlem6  31650  poimirlem7  31651  poimirlem8  31652  poimirlem12  31656  poimirlem13  31657  poimirlem14  31658  poimirlem15  31659  poimirlem16  31660  poimirlem17  31661  poimirlem19  31663  poimirlem20  31664  poimirlem21  31665  poimirlem22  31666  poimirlem23  31667  poimirlem24  31668  poimirlem26  31670  poimirlem28  31672  poimirlem29  31673  poimirlem31  31675  poimirlem32  31676  mblfinlem2  31682  irrapxlem3  35378  irrapxlem4  35379  fzmaxdif  35537  jm2.23  35557  jm2.26lem3  35562  jm2.27dlem2  35571  isprm7  36297  binomcxplemnn0  36335  monoords  37123  elfzolem1  37153  fmul01lt1lem1  37234  fmul01lt1lem2  37235  sumnnodd  37282  dvnmul  37387  dvnprodlem1  37390  dvnprodlem2  37391  iblspltprt  37419  itgspltprt  37425  stoweidlem3  37432  stoweidlem17  37446  stoweidlem20  37449  stoweidlem26  37455  stoweidlem34  37464  fourierdlem11  37549  fourierdlem12  37550  fourierdlem15  37553  fourierdlem25  37563  fourierdlem41  37579  fourierdlem48  37586  fourierdlem49  37587  fourierdlem50  37588  fourierdlem52  37590  fourierdlem54  37592  fourierdlem79  37617  fourierdlem102  37640  fourierdlem114  37652  elaa2lem  37665  etransclem23  37689  etransclem28  37694  etransclem35  37701  etransclem38  37704  iundjiun  37807  iccpartgt  38131  2elfz2melfz  38407  elfzelfzlble  38410  difmodm1lt  39086
  Copyright terms: Public domain W3C validator