Theorem elfzle2 13671

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5105  ‘cfv 6546  (class class class)co 7427   ≤ cle 11354  ℤ_≥cuz 12975  ...cfz 13649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pr 5394  ax-un 7758  ax-cnex 11266  ax-resscn 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-fv 6554  df-ov 7430  df-oprab 7431  df-mpo 7432  df-1st 8008  df-2nd 8009  df-neg 11554  df-z 12704  df-uz 12976  df-fz 13650

This theorem is used by:  elfz1eq  13678  fzdisj  13695  ssfzunsnext  13713  fznatpl1  13722  fzp1disj  13727  uzdisj  13741  fzneuz  13752  fznuz  13753  elfzmlbm  13782  difelfznle  13786  nn0disj  13788  elfzolem1  13849  seqf1olem1  14194  seqf1olem2  14195  bcval4  14461  bcp1nk  14471  hashf1  14612  seqcoll  14619  seqcoll2  14620  isercolllem2  15845  isercoll  15847  summolem2a  15893  fsum0diaglem  15954  mertenslem1  16065  prodmolem2a  16113  binomrisefac  16220  bpoly4  16237  fzm1ndvds  16504  prmind2  16872  prmdvdsfz  16893  isprm7  16896  hashdvds  16964  prmdiveq  16975  prmreclem3  17108  prmreclem5  17110  4sqlem11  17145  4sqlem12  17146  vdwlem1  17171  vdwlem3  17173  vdwlem6  17176  vdwlem9  17179  vdwlem10  17180  mndodconglem  19767  oddvds  19773  gexdvds  19810  coe1tmmul  22608  lebnumii  25299  ovolicc2lem4  25853  voliunlem1  25883  dvfsumle  26353  dvfsumge  26354  dvfsumabs  26355  dvfsumlem3  26360  elply2  26526  coeeq2  26573  aaliou3lem6  26687  birthdaylem2  27292  birthdaylem3  27293  wilthlem1  27407  ftalem5  27416  basellem1  27420  basellem3  27422  ppiprm  27490  chtprm  27492  logfac2  27556  lgsval2lem  27646  lgsqrlem2  27686  lgseisenlem1  27714  lgseisenlem2  27715  lgseisenlem3  27716  lgsquadlem1  27719  lgsquadlem2  27720  2lgslem1a  27730  chebbnd1lem1  27808  dchrvmasumiflem1  27840  mulog2sumlem2  27874  pntrlog2bndlem6  27922  pntpbnd1  27925  pntpbnd2  27926  pntlemh  27938  pntlemj  27942  pntlemf  27944  axlowdimlem16  29547  crctcshwlkn0lem2  30412  crctcshlem4  30421  bcm1n  33440  psgnfzto1stlem  33714  cycpmco2lem6  33745  cycpmco2lem7  33746  smatrcl  34481  submateqlem1  34492  madjusmdetlem2  34513  ballotlemimin  35191  ballotlemsdom  35197  ballotlemsel1i  35198  ballotlemsima  35201  ballotlemfrceq  35214  ballotlemfrcn0  35215  fsum2dsub  35289  reprgt  35303  breprexplemc  35314  erdszelem8  36084  cvmliftlem2  36172  cvmliftlem7  36177  supfz  36621  bcprod  36630  bccolsum  36631  poimirlem2  38680  poimirlem3  38681  poimirlem4  38682  poimirlem6  38684  poimirlem7  38685  poimirlem8  38686  poimirlem12  38690  poimirlem13  38691  poimirlem14  38692  poimirlem15  38693  poimirlem16  38694  poimirlem17  38695  poimirlem19  38697  poimirlem20  38698  poimirlem21  38699  poimirlem22  38700  poimirlem23  38701  poimirlem24  38702  poimirlem26  38704  poimirlem28  38706  poimirlem29  38707  poimirlem31  38709  poimirlem32  38710  mblfinlem2  38716  aks4d1p5  43270  aks4d1p6  43271  aks4d1p8  43277  primrootlekpowne0  43295  aks6d1c1  43306  hashscontpow1  43311  aks6d1c5lem1  43326  sticksstones6  43341  sticksstones7  43342  sticksstones10  43345  sticksstones12a  43347  sticksstones12  43348  bcled  43368  bcle2d  43369  unitscyglem2  43386  unitscyglem4  43388  irrapxlem3  43971  irrapxlem4  43972  fzmaxdif  44128  jm2.23  44143  jm2.26lem3  44148  jm2.27dlem2  44157  binomcxplemnn0  45473  monoords  46452  fmul01lt1lem1  46735  fmul01lt1lem2  46736  sumnnodd  46781  dvnmul  47092  dvnprodlem1  47095  dvnprodlem2  47096  iblspltprt  47122  itgspltprt  47128  stoweidlem3  47152  stoweidlem17  47166  stoweidlem20  47169  stoweidlem26  47175  stoweidlem34  47183  fourierdlem11  47267  fourierdlem12  47268  fourierdlem15  47271  fourierdlem25  47281  fourierdlem41  47297  fourierdlem48  47303  fourierdlem49  47304  fourierdlem50  47305  fourierdlem52  47307  fourierdlem54  47309  fourierdlem79  47334  fourierdlem102  47357  fourierdlem114  47369  elaa2lem  47382  etransclem23  47406  etransclem28  47411  etransclem35  47418  etransclem38  47421  iundjiun  47609  2elfz2melfz  48527  elfzelfzlble  48530  iccpartgt  48648  fmtno4prm  48799