Theorem elfzle2 13564

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 13557	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ≥‘𝐾))
2		eluzle 12888	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝐾) → 𝐾 ≤ 𝑁)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ≤ 𝑁)

Syntax hints:   → wi 4   ∈ wcel 2105   class class class wbr 5147  ‘cfv 6562  (class class class)co 7430   ≤ cle 11293  ℤ_≥cuz 12875  ...cfz 13543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8012  df-2nd 8013  df-neg 11492  df-z 12611  df-uz 12876  df-fz 13544

This theorem is referenced by:  elfz1eq  13571  fzdisj  13587  ssfzunsnext  13605  fznatpl1  13614  fzp1disj  13619  uzdisj  13633  fzneuz  13644  fznuz  13645  elfzmlbm  13674  difelfznle  13678  nn0disj  13680  elfzolem1  13740  seqf1olem1  14078  seqf1olem2  14079  bcval4  14342  bcp1nk  14352  hashf1  14492  seqcoll  14499  seqcoll2  14500  isercolllem2  15698  isercoll  15700  summolem2a  15747  fsum0diaglem  15808  mertenslem1  15916  prodmolem2a  15966  binomrisefac  16074  bpoly4  16091  fzm1ndvds  16355  prmind2  16718  prmdvdsfz  16738  isprm7  16741  hashdvds  16808  prmdiveq  16819  prmreclem3  16951  prmreclem5  16953  4sqlem11  16988  4sqlem12  16989  vdwlem1  17014  vdwlem3  17016  vdwlem6  17019  vdwlem9  17022  vdwlem10  17023  mndodconglem  19573  oddvds  19579  gexdvds  19616  coe1tmmul  22295  lebnumii  25011  ovolicc2lem4  25568  voliunlem1  25598  dvfsumle  26074  dvfsumleOLD  26075  dvfsumge  26076  dvfsumabs  26077  dvfsumlem3  26083  elply2  26249  coeeq2  26295  aaliou3lem6  26404  birthdaylem2  27009  birthdaylem3  27010  wilthlem1  27125  ftalem5  27134  basellem1  27138  basellem3  27140  ppiprm  27208  chtprm  27210  logfac2  27275  lgsval2lem  27365  lgsqrlem2  27405  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgsquadlem1  27438  lgsquadlem2  27439  2lgslem1a  27449  chebbnd1lem1  27527  dchrvmasumiflem1  27559  mulog2sumlem2  27593  pntrlog2bndlem6  27641  pntpbnd1  27644  pntpbnd2  27645  pntlemh  27657  pntlemj  27661  pntlemf  27663  axlowdimlem16  28986  crctcshwlkn0lem2  29840  crctcshlem4  29849  bcm1n  32802  psgnfzto1stlem  33102  cycpmco2lem6  33133  cycpmco2lem7  33134  smatrcl  33756  submateqlem1  33767  madjusmdetlem2  33788  ballotlemimin  34486  ballotlemsdom  34492  ballotlemsel1i  34493  ballotlemsima  34496  ballotlemfrceq  34509  ballotlemfrcn0  34510  fsum2dsub  34600  reprgt  34614  breprexplemc  34625  erdszelem8  35182  cvmliftlem2  35270  cvmliftlem7  35275  supfz  35708  bcprod  35717  bccolsum  35718  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem12  37618  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem26  37632  poimirlem28  37634  poimirlem29  37635  poimirlem31  37637  poimirlem32  37638  mblfinlem2  37644  aks4d1p5  42061  aks4d1p6  42062  aks4d1p8  42068  primrootlekpowne0  42086  aks6d1c1  42097  hashscontpow1  42102  aks6d1c5lem1  42117  sticksstones6  42132  sticksstones7  42133  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  bcled  42159  bcle2d  42160  unitscyglem2  42177  unitscyglem4  42179  metakunt1  42186  metakunt7  42192  metakunt15  42200  metakunt16  42201  metakunt22  42207  metakunt28  42213  metakunt30  42215  irrapxlem3  42811  irrapxlem4  42812  fzmaxdif  42969  jm2.23  42984  jm2.26lem3  42989  jm2.27dlem2  42998  binomcxplemnn0  44344  monoords  45247  fmul01lt1lem1  45539  fmul01lt1lem2  45540  sumnnodd  45585  dvnmul  45898  dvnprodlem1  45901  dvnprodlem2  45902  iblspltprt  45928  itgspltprt  45934  stoweidlem3  45958  stoweidlem17  45972  stoweidlem20  45975  stoweidlem26  45981  stoweidlem34  45989  fourierdlem11  46073  fourierdlem12  46074  fourierdlem15  46077  fourierdlem25  46087  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem52  46113  fourierdlem54  46115  fourierdlem79  46140  fourierdlem102  46163  fourierdlem114  46175  elaa2lem  46188  etransclem23  46212  etransclem28  46217  etransclem35  46224  etransclem38  46227  iundjiun  46415  2elfz2melfz  47267  elfzelfzlble  47270  iccpartgt  47351  fmtno4prm  47499  difmodm1lt  48371