Theorem elfzle2 13456

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  ‘cfv 6500  (class class class)co 7368   ≤ cle 11179  ℤ_≥cuz 12763  ...cfz 13435

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944  df-neg 11379  df-z 12501  df-uz 12764  df-fz 13436

This theorem is referenced by:  elfz1eq  13463  fzdisj  13479  ssfzunsnext  13497  fznatpl1  13506  fzp1disj  13511  uzdisj  13525  fzneuz  13536  fznuz  13537  elfzmlbm  13566  difelfznle  13570  nn0disj  13572  elfzolem1  13632  seqf1olem1  13976  seqf1olem2  13977  bcval4  14242  bcp1nk  14252  hashf1  14392  seqcoll  14399  seqcoll2  14400  isercolllem2  15601  isercoll  15603  summolem2a  15650  fsum0diaglem  15711  mertenslem1  15819  prodmolem2a  15869  binomrisefac  15977  bpoly4  15994  fzm1ndvds  16261  prmind2  16624  prmdvdsfz  16644  isprm7  16647  hashdvds  16714  prmdiveq  16725  prmreclem3  16858  prmreclem5  16860  4sqlem11  16895  4sqlem12  16896  vdwlem1  16921  vdwlem3  16923  vdwlem6  16926  vdwlem9  16929  vdwlem10  16930  mndodconglem  19482  oddvds  19488  gexdvds  19525  coe1tmmul  22231  lebnumii  24933  ovolicc2lem4  25489  voliunlem1  25519  dvfsumle  25994  dvfsumleOLD  25995  dvfsumge  25996  dvfsumabs  25997  dvfsumlem3  26003  elply2  26169  coeeq2  26215  aaliou3lem6  26324  birthdaylem2  26930  birthdaylem3  26931  wilthlem1  27046  ftalem5  27055  basellem1  27059  basellem3  27061  ppiprm  27129  chtprm  27131  logfac2  27196  lgsval2lem  27286  lgsqrlem2  27326  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgsquadlem1  27359  lgsquadlem2  27360  2lgslem1a  27370  chebbnd1lem1  27448  dchrvmasumiflem1  27480  mulog2sumlem2  27514  pntrlog2bndlem6  27562  pntpbnd1  27565  pntpbnd2  27566  pntlemh  27578  pntlemj  27582  pntlemf  27584  axlowdimlem16  29042  crctcshwlkn0lem2  29896  crctcshlem4  29905  bcm1n  32886  psgnfzto1stlem  33194  cycpmco2lem6  33225  cycpmco2lem7  33226  smatrcl  33974  submateqlem1  33985  madjusmdetlem2  34006  ballotlemimin  34684  ballotlemsdom  34690  ballotlemsel1i  34691  ballotlemsima  34694  ballotlemfrceq  34707  ballotlemfrcn0  34708  fsum2dsub  34785  reprgt  34799  breprexplemc  34810  erdszelem8  35414  cvmliftlem2  35502  cvmliftlem7  35507  supfz  35945  bcprod  35954  bccolsum  35955  poimirlem2  37873  poimirlem3  37874  poimirlem4  37875  poimirlem6  37877  poimirlem7  37878  poimirlem8  37879  poimirlem12  37883  poimirlem13  37884  poimirlem14  37885  poimirlem15  37886  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem21  37892  poimirlem22  37893  poimirlem23  37894  poimirlem24  37895  poimirlem26  37897  poimirlem28  37899  poimirlem29  37900  poimirlem31  37902  poimirlem32  37903  mblfinlem2  37909  aks4d1p5  42450  aks4d1p6  42451  aks4d1p8  42457  primrootlekpowne0  42475  aks6d1c1  42486  hashscontpow1  42491  aks6d1c5lem1  42506  sticksstones6  42521  sticksstones7  42522  sticksstones10  42525  sticksstones12a  42527  sticksstones12  42528  bcled  42548  bcle2d  42549  unitscyglem2  42566  unitscyglem4  42568  irrapxlem3  43181  irrapxlem4  43182  fzmaxdif  43338  jm2.23  43353  jm2.26lem3  43358  jm2.27dlem2  43367  binomcxplemnn0  44705  monoords  45659  fmul01lt1lem1  45944  fmul01lt1lem2  45945  sumnnodd  45990  dvnmul  46301  dvnprodlem1  46304  dvnprodlem2  46305  iblspltprt  46331  itgspltprt  46337  stoweidlem3  46361  stoweidlem17  46375  stoweidlem20  46378  stoweidlem26  46384  stoweidlem34  46392  fourierdlem11  46476  fourierdlem12  46477  fourierdlem15  46480  fourierdlem25  46490  fourierdlem41  46506  fourierdlem48  46512  fourierdlem49  46513  fourierdlem50  46514  fourierdlem52  46516  fourierdlem54  46518  fourierdlem79  46543  fourierdlem102  46566  fourierdlem114  46578  elaa2lem  46591  etransclem23  46615  etransclem28  46620  etransclem35  46627  etransclem38  46630  iundjiun  46818  2elfz2melfz  47678  elfzelfzlble  47681  iccpartgt  47787  fmtno4prm  47935