Theorem elfzle2 13504

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5148  ‘cfv 6543  (class class class)co 7408   ≤ cle 11248  ℤ_≥cuz 12821  ...cfz 13483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7974  df-2nd 7975  df-neg 11446  df-z 12558  df-uz 12822  df-fz 13484

This theorem is referenced by:  elfz1eq  13511  fzdisj  13527  ssfzunsnext  13545  fznatpl1  13554  fzp1disj  13559  uzdisj  13573  fzneuz  13581  fznuz  13582  elfzmlbm  13610  difelfznle  13614  nn0disj  13616  seqf1olem1  14006  seqf1olem2  14007  bcval4  14266  bcp1nk  14276  hashf1  14417  seqcoll  14424  seqcoll2  14425  isercolllem2  15611  isercoll  15613  summolem2a  15660  fsum0diaglem  15721  mertenslem1  15829  prodmolem2a  15877  binomrisefac  15985  bpoly4  16002  fzm1ndvds  16264  prmind2  16621  prmdvdsfz  16641  isprm7  16644  hashdvds  16707  prmdiveq  16718  prmreclem3  16850  prmreclem5  16852  4sqlem11  16887  4sqlem12  16888  vdwlem1  16913  vdwlem3  16915  vdwlem6  16918  vdwlem9  16921  vdwlem10  16922  mndodconglem  19408  oddvds  19414  gexdvds  19451  coe1tmmul  21798  lebnumii  24481  ovolicc2lem4  25036  voliunlem1  25066  dvfsumle  25537  dvfsumge  25538  dvfsumabs  25539  dvfsumlem3  25544  elply2  25709  coeeq2  25755  aaliou3lem6  25860  birthdaylem2  26454  birthdaylem3  26455  wilthlem1  26569  ftalem5  26578  basellem1  26582  basellem3  26584  ppiprm  26652  chtprm  26654  logfac2  26717  lgsval2lem  26807  lgsqrlem2  26847  lgseisenlem1  26875  lgseisenlem2  26876  lgseisenlem3  26877  lgsquadlem1  26880  lgsquadlem2  26881  2lgslem1a  26891  chebbnd1lem1  26969  dchrvmasumiflem1  27001  mulog2sumlem2  27035  pntrlog2bndlem6  27083  pntpbnd1  27086  pntpbnd2  27087  pntlemh  27099  pntlemj  27103  pntlemf  27105  axlowdimlem16  28212  crctcshwlkn0lem2  29062  crctcshlem4  29071  bcm1n  32001  psgnfzto1stlem  32254  cycpmco2lem6  32285  cycpmco2lem7  32286  smatrcl  32771  submateqlem1  32782  madjusmdetlem2  32803  ballotlemimin  33499  ballotlemsdom  33505  ballotlemsel1i  33506  ballotlemsima  33509  ballotlemfrceq  33522  ballotlemfrcn0  33523  fsum2dsub  33614  reprgt  33628  breprexplemc  33639  erdszelem8  34184  cvmliftlem2  34272  cvmliftlem7  34277  supfz  34693  bcprod  34703  bccolsum  34704  gg-dvfsumle  35177  poimirlem2  36485  poimirlem3  36486  poimirlem4  36487  poimirlem6  36489  poimirlem7  36490  poimirlem8  36491  poimirlem12  36495  poimirlem13  36496  poimirlem14  36497  poimirlem15  36498  poimirlem16  36499  poimirlem17  36500  poimirlem19  36502  poimirlem20  36503  poimirlem21  36504  poimirlem22  36505  poimirlem23  36506  poimirlem24  36507  poimirlem26  36509  poimirlem28  36511  poimirlem29  36512  poimirlem31  36514  poimirlem32  36515  mblfinlem2  36521  aks4d1p5  40940  aks4d1p6  40941  aks4d1p8  40947  sticksstones6  40962  sticksstones7  40963  sticksstones10  40966  sticksstones12a  40968  sticksstones12  40969  metakunt1  40980  metakunt7  40986  metakunt15  40994  metakunt16  40995  metakunt22  41001  metakunt28  41007  metakunt30  41009  irrapxlem3  41552  irrapxlem4  41553  fzmaxdif  41710  jm2.23  41725  jm2.26lem3  41730  jm2.27dlem2  41739  binomcxplemnn0  43098  monoords  43997  elfzolem1  44021  fmul01lt1lem1  44290  fmul01lt1lem2  44291  sumnnodd  44336  dvnmul  44649  dvnprodlem1  44652  dvnprodlem2  44653  iblspltprt  44679  itgspltprt  44685  stoweidlem3  44709  stoweidlem17  44723  stoweidlem20  44726  stoweidlem26  44732  stoweidlem34  44740  fourierdlem11  44824  fourierdlem12  44825  fourierdlem15  44828  fourierdlem25  44838  fourierdlem41  44854  fourierdlem48  44860  fourierdlem49  44861  fourierdlem50  44862  fourierdlem52  44864  fourierdlem54  44866  fourierdlem79  44891  fourierdlem102  44914  fourierdlem114  44926  elaa2lem  44939  etransclem23  44963  etransclem28  44968  etransclem35  44975  etransclem38  44978  iundjiun  45166  2elfz2melfz  46016  elfzelfzlble  46019  iccpartgt  46085  fmtno4prm  46233  difmodm1lt  47198