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

Theorem elfzle2 11838
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 11832 . 2  |-  ( K  e.  ( M ... N )  ->  N  e.  ( ZZ>= `  K )
)
2 eluzle 11205 . 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 1898   class class class wbr 4418   ` cfv 5605  (class class class)co 6320    <_ cle 9707   ZZ>=cuz 11193   ...cfz 11819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-cnex 9626  ax-resscn 9627
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-fv 5613  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-1st 6825  df-2nd 6826  df-neg 9894  df-z 10972  df-uz 11194  df-fz 11820
This theorem is referenced by:  elfz1eq  11845  fzdisj  11861  fznatpl1  11885  fzp1disj  11889  uzdisj  11902  fzneuz  11910  fznuz  11911  elfzmlbm  11936  difelfznle  11941  nn0disj  11943  seqf1olem1  12290  seqf1olem2  12291  bcval4  12530  bcp1nk  12540  hashf1  12659  seqcoll  12666  seqcoll2  12667  isercolllem2  13784  isercoll  13786  summolem2a  13836  fsum0diaglem  13892  mertenslem1  13995  prodmolem2a  14043  binomrisefac  14150  bpoly4  14167  fzm1ndvds  14412  prmind2  14690  prmdvdsfz  14704  hashdvds  14778  prmdiveq  14789  prmreclem3  14917  prmreclem5  14919  4sqlem11  14954  4sqlem12  14955  vdwlem1  14986  vdwlem3  14988  vdwlem6  14991  vdwlem9  14994  vdwlem10  14995  strlemor1  15272  mndodconglem  17245  oddvds  17251  gexdvds  17290  coe1tmmul  18925  lebnumii  22052  ovolicc2lem4OLD  22528  ovolicc2lem4  22529  voliunlem1  22559  dvfsumle  23029  dvfsumge  23030  dvfsumabs  23031  dvfsumlem3  23036  elply2  23206  coeeq2  23252  aaliou3lem6  23360  birthdaylem2  23934  birthdaylem3  23935  wilthlem1  24049  ftalem5  24057  ftalem5OLD  24059  basellem1  24063  basellem3  24065  ppiprm  24134  chtprm  24136  logfac2  24201  lgsval2lem  24290  lgsqrlem2  24326  lgseisenlem1  24333  lgseisenlem2  24334  lgseisenlem3  24335  lgsquadlem1  24338  lgsquadlem2  24339  chebbnd1lem1  24363  dchrvmasumiflem1  24395  mulog2sumlem2  24429  pntrlog2bndlem6  24477  pntpbnd1  24480  pntpbnd2  24481  pntlemh  24493  pntlemj  24497  pntlemf  24499  axlowdimlem16  25043  eupap1  25760  bcm1n  28423  psgnfzto1stlem  28664  smatrcl  28673  submateqlem1  28684  madjusmdetlem2  28705  ballotlemimin  29388  ballotlemsdom  29394  ballotlemsel1i  29395  ballotlemsima  29398  ballotlemfrceq  29411  ballotlemfrcn0  29412  ballotlemiminOLD  29426  ballotlemsdomOLD  29432  ballotlemsel1iOLD  29433  ballotlemsimaOLD  29436  ballotlemfrceqOLD  29449  ballotlemfrcn0OLD  29450  erdszelem8  29971  cvmliftlem2  30059  cvmliftlem7  30064  supfz  30412  bcprod  30424  bccolsum  30425  poimirlem2  31988  poimirlem3  31989  poimirlem4  31990  poimirlem6  31992  poimirlem7  31993  poimirlem8  31994  poimirlem12  31998  poimirlem13  31999  poimirlem14  32000  poimirlem15  32001  poimirlem16  32002  poimirlem17  32003  poimirlem19  32005  poimirlem20  32006  poimirlem21  32007  poimirlem22  32008  poimirlem23  32009  poimirlem24  32010  poimirlem26  32012  poimirlem28  32014  poimirlem29  32015  poimirlem31  32017  poimirlem32  32018  mblfinlem2  32024  irrapxlem3  35714  irrapxlem4  35715  fzmaxdif  35877  jm2.23  35897  jm2.26lem3  35902  jm2.27dlem2  35911  isprm7  36705  binomcxplemnn0  36743  monoords  37589  elfzolem1  37619  fmul01lt1lem1  37748  fmul01lt1lem2  37749  sumnnodd  37796  dvnmul  37904  dvnprodlem1  37907  dvnprodlem2  37908  iblspltprt  37936  itgspltprt  37942  stoweidlem3  37964  stoweidlem17  37978  stoweidlem20  37981  stoweidlem26  37987  stoweidlem34  37996  fourierdlem11  38081  fourierdlem12  38082  fourierdlem15  38085  fourierdlem25  38095  fourierdlem41  38112  fourierdlem48  38119  fourierdlem49  38120  fourierdlem50  38121  fourierdlem52  38123  fourierdlem54  38125  fourierdlem79  38150  fourierdlem102  38173  fourierdlem114  38185  elaa2lem  38198  elaa2lemOLD  38199  etransclem23  38223  etransclem28  38228  etransclem35  38235  etransclem38  38238  iundjiun  38403  iccpartgt  38876  2elfz2melfz  39196  elfzelfzlble  39199  difmodm1lt  40694
  Copyright terms: Public domain W3C validator