Theorem elfzle2 13505

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5149  ‘cfv 6544  (class class class)co 7409   ≤ cle 11249  ℤ_≥cuz 12822  ...cfz 13484

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 5300  ax-nul 5307  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167

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 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-1st 7975  df-2nd 7976  df-neg 11447  df-z 12559  df-uz 12823  df-fz 13485

This theorem is referenced by:  elfz1eq  13512  fzdisj  13528  ssfzunsnext  13546  fznatpl1  13555  fzp1disj  13560  uzdisj  13574  fzneuz  13582  fznuz  13583  elfzmlbm  13611  difelfznle  13615  nn0disj  13617  seqf1olem1  14007  seqf1olem2  14008  bcval4  14267  bcp1nk  14277  hashf1  14418  seqcoll  14425  seqcoll2  14426  isercolllem2  15612  isercoll  15614  summolem2a  15661  fsum0diaglem  15722  mertenslem1  15830  prodmolem2a  15878  binomrisefac  15986  bpoly4  16003  fzm1ndvds  16265  prmind2  16622  prmdvdsfz  16642  isprm7  16645  hashdvds  16708  prmdiveq  16719  prmreclem3  16851  prmreclem5  16853  4sqlem11  16888  4sqlem12  16889  vdwlem1  16914  vdwlem3  16916  vdwlem6  16919  vdwlem9  16922  vdwlem10  16923  mndodconglem  19409  oddvds  19415  gexdvds  19452  coe1tmmul  21799  lebnumii  24482  ovolicc2lem4  25037  voliunlem1  25067  dvfsumle  25538  dvfsumge  25539  dvfsumabs  25540  dvfsumlem3  25545  elply2  25710  coeeq2  25756  aaliou3lem6  25861  birthdaylem2  26457  birthdaylem3  26458  wilthlem1  26572  ftalem5  26581  basellem1  26585  basellem3  26587  ppiprm  26655  chtprm  26657  logfac2  26720  lgsval2lem  26810  lgsqrlem2  26850  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem3  26880  lgsquadlem1  26883  lgsquadlem2  26884  2lgslem1a  26894  chebbnd1lem1  26972  dchrvmasumiflem1  27004  mulog2sumlem2  27038  pntrlog2bndlem6  27086  pntpbnd1  27089  pntpbnd2  27090  pntlemh  27102  pntlemj  27106  pntlemf  27108  axlowdimlem16  28215  crctcshwlkn0lem2  29065  crctcshlem4  29074  bcm1n  32006  psgnfzto1stlem  32259  cycpmco2lem6  32290  cycpmco2lem7  32291  smatrcl  32776  submateqlem1  32787  madjusmdetlem2  32808  ballotlemimin  33504  ballotlemsdom  33510  ballotlemsel1i  33511  ballotlemsima  33514  ballotlemfrceq  33527  ballotlemfrcn0  33528  fsum2dsub  33619  reprgt  33633  breprexplemc  33644  erdszelem8  34189  cvmliftlem2  34277  cvmliftlem7  34282  supfz  34698  bcprod  34708  bccolsum  34709  gg-dvfsumle  35182  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem12  36500  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem23  36511  poimirlem24  36512  poimirlem26  36514  poimirlem28  36516  poimirlem29  36517  poimirlem31  36519  poimirlem32  36520  mblfinlem2  36526  aks4d1p5  40945  aks4d1p6  40946  aks4d1p8  40952  sticksstones6  40967  sticksstones7  40968  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  metakunt1  40985  metakunt7  40991  metakunt15  40999  metakunt16  41000  metakunt22  41006  metakunt28  41012  metakunt30  41014  irrapxlem3  41562  irrapxlem4  41563  fzmaxdif  41720  jm2.23  41735  jm2.26lem3  41740  jm2.27dlem2  41749  binomcxplemnn0  43108  monoords  44007  elfzolem1  44031  fmul01lt1lem1  44300  fmul01lt1lem2  44301  sumnnodd  44346  dvnmul  44659  dvnprodlem1  44662  dvnprodlem2  44663  iblspltprt  44689  itgspltprt  44695  stoweidlem3  44719  stoweidlem17  44733  stoweidlem20  44736  stoweidlem26  44742  stoweidlem34  44750  fourierdlem11  44834  fourierdlem12  44835  fourierdlem15  44838  fourierdlem25  44848  fourierdlem41  44864  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem52  44874  fourierdlem54  44876  fourierdlem79  44901  fourierdlem102  44924  fourierdlem114  44936  elaa2lem  44949  etransclem23  44973  etransclem28  44978  etransclem35  44985  etransclem38  44988  iundjiun  45176  2elfz2melfz  46026  elfzelfzlble  46029  iccpartgt  46095  fmtno4prm  46243  difmodm1lt  47208