Theorem elfzle2 13434

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5093  ‘cfv 6487  (class class class)co 7352   ≤ cle 11153  ℤ_≥cuz 12738  ...cfz 13413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674  ax-cnex 11068  ax-resscn 11069

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-fv 6495  df-ov 7355  df-oprab 7356  df-mpo 7357  df-1st 7927  df-2nd 7928  df-neg 11353  df-z 12475  df-uz 12739  df-fz 13414

This theorem is referenced by:  elfz1eq  13441  fzdisj  13457  ssfzunsnext  13475  fznatpl1  13484  fzp1disj  13489  uzdisj  13503  fzneuz  13514  fznuz  13515  elfzmlbm  13544  difelfznle  13548  nn0disj  13550  elfzolem1  13610  seqf1olem1  13954  seqf1olem2  13955  bcval4  14220  bcp1nk  14230  hashf1  14370  seqcoll  14377  seqcoll2  14378  isercolllem2  15579  isercoll  15581  summolem2a  15628  fsum0diaglem  15689  mertenslem1  15797  prodmolem2a  15847  binomrisefac  15955  bpoly4  15972  fzm1ndvds  16239  prmind2  16602  prmdvdsfz  16622  isprm7  16625  hashdvds  16692  prmdiveq  16703  prmreclem3  16836  prmreclem5  16838  4sqlem11  16873  4sqlem12  16874  vdwlem1  16899  vdwlem3  16901  vdwlem6  16904  vdwlem9  16907  vdwlem10  16908  mndodconglem  19459  oddvds  19465  gexdvds  19502  coe1tmmul  22197  lebnumii  24898  ovolicc2lem4  25454  voliunlem1  25484  dvfsumle  25959  dvfsumleOLD  25960  dvfsumge  25961  dvfsumabs  25962  dvfsumlem3  25968  elply2  26134  coeeq2  26180  aaliou3lem6  26289  birthdaylem2  26895  birthdaylem3  26896  wilthlem1  27011  ftalem5  27020  basellem1  27024  basellem3  27026  ppiprm  27094  chtprm  27096  logfac2  27161  lgsval2lem  27251  lgsqrlem2  27291  lgseisenlem1  27319  lgseisenlem2  27320  lgseisenlem3  27321  lgsquadlem1  27324  lgsquadlem2  27325  2lgslem1a  27335  chebbnd1lem1  27413  dchrvmasumiflem1  27445  mulog2sumlem2  27479  pntrlog2bndlem6  27527  pntpbnd1  27530  pntpbnd2  27531  pntlemh  27543  pntlemj  27547  pntlemf  27549  axlowdimlem16  28942  crctcshwlkn0lem2  29796  crctcshlem4  29805  bcm1n  32784  psgnfzto1stlem  33076  cycpmco2lem6  33107  cycpmco2lem7  33108  smatrcl  33816  submateqlem1  33827  madjusmdetlem2  33848  ballotlemimin  34526  ballotlemsdom  34532  ballotlemsel1i  34533  ballotlemsima  34536  ballotlemfrceq  34549  ballotlemfrcn0  34550  fsum2dsub  34627  reprgt  34641  breprexplemc  34652  erdszelem8  35249  cvmliftlem2  35337  cvmliftlem7  35342  supfz  35780  bcprod  35789  bccolsum  35790  poimirlem2  37668  poimirlem3  37669  poimirlem4  37670  poimirlem6  37672  poimirlem7  37673  poimirlem8  37674  poimirlem12  37678  poimirlem13  37679  poimirlem14  37680  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem19  37685  poimirlem20  37686  poimirlem21  37687  poimirlem22  37688  poimirlem23  37689  poimirlem24  37690  poimirlem26  37692  poimirlem28  37694  poimirlem29  37695  poimirlem31  37697  poimirlem32  37698  mblfinlem2  37704  aks4d1p5  42179  aks4d1p6  42180  aks4d1p8  42186  primrootlekpowne0  42204  aks6d1c1  42215  hashscontpow1  42220  aks6d1c5lem1  42235  sticksstones6  42250  sticksstones7  42251  sticksstones10  42254  sticksstones12a  42256  sticksstones12  42257  bcled  42277  bcle2d  42278  unitscyglem2  42295  unitscyglem4  42297  irrapxlem3  42922  irrapxlem4  42923  fzmaxdif  43079  jm2.23  43094  jm2.26lem3  43099  jm2.27dlem2  43108  binomcxplemnn0  44447  monoords  45403  fmul01lt1lem1  45689  fmul01lt1lem2  45690  sumnnodd  45735  dvnmul  46046  dvnprodlem1  46049  dvnprodlem2  46050  iblspltprt  46076  itgspltprt  46082  stoweidlem3  46106  stoweidlem17  46120  stoweidlem20  46123  stoweidlem26  46129  stoweidlem34  46137  fourierdlem11  46221  fourierdlem12  46222  fourierdlem15  46225  fourierdlem25  46235  fourierdlem41  46251  fourierdlem48  46257  fourierdlem49  46258  fourierdlem50  46259  fourierdlem52  46261  fourierdlem54  46263  fourierdlem79  46288  fourierdlem102  46311  fourierdlem114  46323  elaa2lem  46336  etransclem23  46360  etransclem28  46365  etransclem35  46372  etransclem38  46375  iundjiun  46563  2elfz2melfz  47423  elfzelfzlble  47426  iccpartgt  47532  fmtno4prm  47680