Theorem elfzle2 13556

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

Step	Hyp	Ref	Expression
1		elfzuz3 13549	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))
2		eluzle 12875	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝐾 ≤ 𝑁)
3	1, 2	syl 18	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ≤ 𝑁)

Syntax hints:   → wi 4   ∈ wcel 2149   class class class wbr 5113  ‘cfv 6537  (class class class)co 7411   ≤ cle 11244  ℤ_≥cuz 12862  ...cfz 13535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-resscn 11157

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7986  df-2nd 7987  df-neg 11444  df-z 12592  df-uz 12863  df-fz 13536

This theorem is referenced by:  elfz1eq  13563  fzdisj  13579  ssfzunsnext  13597  fznatpl1  13606  fzp1disj  13611  uzdisj  13625  fzneuz  13636  fznuz  13637  elfzmlbm  13666  difelfznle  13670  nn0disj  13672  elfzolem1  13733  seqf1olem1  14077  seqf1olem2  14078  bcval4  14343  bcp1nk  14353  hashf1  14494  seqcoll  14501  seqcoll2  14502  isercolllem2  15717  isercoll  15719  summolem2a  15766  fsum0diaglem  15827  mertenslem1  15938  prodmolem2a  15988  binomrisefac  16096  bpoly4  16113  fzm1ndvds  16380  prmind2  16743  prmdvdsfz  16764  isprm7  16767  hashdvds  16834  prmdiveq  16845  prmreclem3  16978  prmreclem5  16980  4sqlem11  17015  4sqlem12  17016  vdwlem1  17041  vdwlem3  17043  vdwlem6  17046  vdwlem9  17049  vdwlem10  17050  mndodconglem  19611  oddvds  19617  gexdvds  19654  coe1tmmul  22407  lebnumii  25094  ovolicc2lem4  25648  voliunlem1  25678  dvfsumle  26149  dvfsumge  26150  dvfsumabs  26151  dvfsumlem3  26156  elply2  26322  coeeq2  26368  aaliou3lem6  26478  birthdaylem2  27083  birthdaylem3  27084  wilthlem1  27198  ftalem5  27207  basellem1  27211  basellem3  27213  ppiprm  27281  chtprm  27283  logfac2  27347  lgsval2lem  27437  lgsqrlem2  27477  lgseisenlem1  27505  lgseisenlem2  27506  lgseisenlem3  27507  lgsquadlem1  27510  lgsquadlem2  27511  2lgslem1a  27521  chebbnd1lem1  27599  dchrvmasumiflem1  27631  mulog2sumlem2  27665  pntrlog2bndlem6  27713  pntpbnd1  27716  pntpbnd2  27717  pntlemh  27729  pntlemj  27733  pntlemf  27735  axlowdimlem16  29248  crctcshwlkn0lem2  30101  crctcshlem4  30110  bcm1n  33081  psgnfzto1stlem  33361  cycpmco2lem6  33392  cycpmco2lem7  33393  smatrcl  34131  submateqlem1  34142  madjusmdetlem2  34163  ballotlemimin  34841  ballotlemsdom  34847  ballotlemsel1i  34848  ballotlemsima  34851  ballotlemfrceq  34864  ballotlemfrcn0  34865  fsum2dsub  34939  reprgt  34953  breprexplemc  34964  erdszelem8  35589  cvmliftlem2  35677  cvmliftlem7  35682  supfz  36120  bcprod  36129  bccolsum  36130  poimirlem2  38161  poimirlem3  38162  poimirlem4  38163  poimirlem6  38165  poimirlem7  38166  poimirlem8  38167  poimirlem12  38171  poimirlem13  38172  poimirlem14  38173  poimirlem15  38174  poimirlem16  38175  poimirlem17  38176  poimirlem19  38178  poimirlem20  38179  poimirlem21  38180  poimirlem22  38181  poimirlem23  38182  poimirlem24  38183  poimirlem26  38185  poimirlem28  38187  poimirlem29  38188  poimirlem31  38190  poimirlem32  38191  mblfinlem2  38197  aks4d1p5  42737  aks4d1p6  42738  aks4d1p8  42744  primrootlekpowne0  42762  aks6d1c1  42773  hashscontpow1  42778  aks6d1c5lem1  42793  sticksstones6  42808  sticksstones7  42809  sticksstones10  42812  sticksstones12a  42814  sticksstones12  42815  bcled  42835  bcle2d  42836  unitscyglem2  42853  unitscyglem4  42855  irrapxlem3  43443  irrapxlem4  43444  fzmaxdif  43600  jm2.23  43615  jm2.26lem3  43620  jm2.27dlem2  43629  binomcxplemnn0  44951  monoords  45908  fmul01lt1lem1  46192  fmul01lt1lem2  46193  sumnnodd  46238  dvnmul  46549  dvnprodlem1  46552  dvnprodlem2  46553  iblspltprt  46579  itgspltprt  46585  stoweidlem3  46609  stoweidlem17  46623  stoweidlem20  46626  stoweidlem26  46632  stoweidlem34  46640  fourierdlem11  46724  fourierdlem12  46725  fourierdlem15  46728  fourierdlem25  46738  fourierdlem41  46754  fourierdlem48  46760  fourierdlem49  46761  fourierdlem50  46762  fourierdlem52  46764  fourierdlem54  46766  fourierdlem79  46791  fourierdlem102  46814  fourierdlem114  46826  elaa2lem  46839  etransclem23  46863  etransclem28  46868  etransclem35  46875  etransclem38  46878  iundjiun  47066  2elfz2melfz  47944  elfzelfzlble  47947  iccpartgt  48065  fmtno4prm  48216