Theorem elfzle2 13476

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ‘cfv 6493  (class class class)co 7361   ≤ cle 11174  ℤ_≥cuz 12782  ...cfz 13455

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 5232  ax-nul 5242  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089

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 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7936  df-2nd 7937  df-neg 11374  df-z 12519  df-uz 12783  df-fz 13456

This theorem is referenced by:  elfz1eq  13483  fzdisj  13499  ssfzunsnext  13517  fznatpl1  13526  fzp1disj  13531  uzdisj  13545  fzneuz  13556  fznuz  13557  elfzmlbm  13586  difelfznle  13590  nn0disj  13592  elfzolem1  13653  seqf1olem1  13997  seqf1olem2  13998  bcval4  14263  bcp1nk  14273  hashf1  14413  seqcoll  14420  seqcoll2  14421  isercolllem2  15622  isercoll  15624  summolem2a  15671  fsum0diaglem  15732  mertenslem1  15843  prodmolem2a  15893  binomrisefac  16001  bpoly4  16018  fzm1ndvds  16285  prmind2  16648  prmdvdsfz  16669  isprm7  16672  hashdvds  16739  prmdiveq  16750  prmreclem3  16883  prmreclem5  16885  4sqlem11  16920  4sqlem12  16921  vdwlem1  16946  vdwlem3  16948  vdwlem6  16951  vdwlem9  16954  vdwlem10  16955  mndodconglem  19510  oddvds  19516  gexdvds  19553  coe1tmmul  22255  lebnumii  24946  ovolicc2lem4  25500  voliunlem1  25530  dvfsumle  26001  dvfsumge  26002  dvfsumabs  26003  dvfsumlem3  26008  elply2  26174  coeeq2  26220  aaliou3lem6  26328  birthdaylem2  26932  birthdaylem3  26933  wilthlem1  27048  ftalem5  27057  basellem1  27061  basellem3  27063  ppiprm  27131  chtprm  27133  logfac2  27197  lgsval2lem  27287  lgsqrlem2  27327  lgseisenlem1  27355  lgseisenlem2  27356  lgseisenlem3  27357  lgsquadlem1  27360  lgsquadlem2  27361  2lgslem1a  27371  chebbnd1lem1  27449  dchrvmasumiflem1  27481  mulog2sumlem2  27515  pntrlog2bndlem6  27563  pntpbnd1  27566  pntpbnd2  27567  pntlemh  27579  pntlemj  27583  pntlemf  27585  axlowdimlem16  29043  crctcshwlkn0lem2  29897  crctcshlem4  29906  bcm1n  32886  psgnfzto1stlem  33179  cycpmco2lem6  33210  cycpmco2lem7  33211  smatrcl  33959  submateqlem1  33970  madjusmdetlem2  33991  ballotlemimin  34669  ballotlemsdom  34675  ballotlemsel1i  34676  ballotlemsima  34679  ballotlemfrceq  34692  ballotlemfrcn0  34693  fsum2dsub  34770  reprgt  34784  breprexplemc  34795  erdszelem8  35399  cvmliftlem2  35487  cvmliftlem7  35492  supfz  35930  bcprod  35939  bccolsum  35940  poimirlem2  37960  poimirlem3  37961  poimirlem4  37962  poimirlem6  37964  poimirlem7  37965  poimirlem8  37966  poimirlem12  37970  poimirlem13  37971  poimirlem14  37972  poimirlem15  37973  poimirlem16  37974  poimirlem17  37975  poimirlem19  37977  poimirlem20  37978  poimirlem21  37979  poimirlem22  37980  poimirlem23  37981  poimirlem24  37982  poimirlem26  37984  poimirlem28  37986  poimirlem29  37987  poimirlem31  37989  poimirlem32  37990  mblfinlem2  37996  aks4d1p5  42536  aks4d1p6  42537  aks4d1p8  42543  primrootlekpowne0  42561  aks6d1c1  42572  hashscontpow1  42577  aks6d1c5lem1  42592  sticksstones6  42607  sticksstones7  42608  sticksstones10  42611  sticksstones12a  42613  sticksstones12  42614  bcled  42634  bcle2d  42635  unitscyglem2  42652  unitscyglem4  42654  irrapxlem3  43273  irrapxlem4  43274  fzmaxdif  43430  jm2.23  43445  jm2.26lem3  43450  jm2.27dlem2  43459  binomcxplemnn0  44797  monoords  45751  fmul01lt1lem1  46035  fmul01lt1lem2  46036  sumnnodd  46081  dvnmul  46392  dvnprodlem1  46395  dvnprodlem2  46396  iblspltprt  46422  itgspltprt  46428  stoweidlem3  46452  stoweidlem17  46466  stoweidlem20  46469  stoweidlem26  46475  stoweidlem34  46483  fourierdlem11  46567  fourierdlem12  46568  fourierdlem15  46571  fourierdlem25  46581  fourierdlem41  46597  fourierdlem48  46603  fourierdlem49  46604  fourierdlem50  46605  fourierdlem52  46607  fourierdlem54  46609  fourierdlem79  46634  fourierdlem102  46657  fourierdlem114  46669  elaa2lem  46682  etransclem23  46706  etransclem28  46711  etransclem35  46718  etransclem38  46721  iundjiun  46909  2elfz2melfz  47781  elfzelfzlble  47784  iccpartgt  47902  fmtno4prm  48053