Theorem elfzle2 12761

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

Syntax hints:   → wi 4   ∈ wcel 2080   class class class wbr 4964  ‘cfv 6228  (class class class)co 7019   ≤ cle 10525  ℤ_≥cuz 12093  ...cfz 12742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322  ax-cnex 10442  ax-resscn 10443

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-ral 3109  df-rex 3110  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-op 4481  df-uni 4748  df-iun 4829  df-br 4965  df-opab 5027  df-mpt 5044  df-id 5351  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-fv 6236  df-ov 7022  df-oprab 7023  df-mpo 7024  df-1st 7548  df-2nd 7549  df-neg 10722  df-z 11832  df-uz 12094  df-fz 12743

This theorem is referenced by:  elfz1eq  12768  fzdisj  12784  ssfzunsnext  12802  fznatpl1  12811  fzp1disj  12816  uzdisj  12830  fzneuz  12838  fznuz  12839  elfzmlbm  12867  difelfznle  12871  nn0disj  12873  seqf1olem1  13259  seqf1olem2  13260  bcval4  13517  bcp1nk  13527  hashf1  13663  seqcoll  13670  seqcoll2  13671  isercolllem2  14856  isercoll  14858  summolem2a  14905  fsum0diaglem  14964  mertenslem1  15073  prodmolem2a  15121  binomrisefac  15229  bpoly4  15246  fzm1ndvds  15505  prmind2  15858  prmdvdsfz  15878  isprm7  15881  hashdvds  15941  prmdiveq  15952  prmreclem3  16083  prmreclem5  16085  4sqlem11  16120  4sqlem12  16121  vdwlem1  16146  vdwlem3  16148  vdwlem6  16151  vdwlem9  16154  vdwlem10  16155  mndodconglem  18400  oddvds  18406  gexdvds  18439  coe1tmmul  20128  lebnumii  23253  ovolicc2lem4  23804  voliunlem1  23834  dvfsumle  24301  dvfsumge  24302  dvfsumabs  24303  dvfsumlem3  24308  elply2  24469  coeeq2  24515  aaliou3lem6  24620  birthdaylem2  25212  birthdaylem3  25213  wilthlem1  25327  ftalem5  25336  basellem1  25340  basellem3  25342  ppiprm  25410  chtprm  25412  logfac2  25475  lgsval2lem  25565  lgsqrlem2  25605  lgseisenlem1  25633  lgseisenlem2  25634  lgseisenlem3  25635  lgsquadlem1  25638  lgsquadlem2  25639  2lgslem1a  25649  chebbnd1lem1  25727  dchrvmasumiflem1  25759  mulog2sumlem2  25793  pntrlog2bndlem6  25841  pntpbnd1  25844  pntpbnd2  25845  pntlemh  25857  pntlemj  25861  pntlemf  25863  axlowdimlem16  26426  crctcshwlkn0lem2  27271  crctcshlem4  27280  bcm1n  30196  psgnfzto1stlem  30656  smatrcl  30668  submateqlem1  30679  madjusmdetlem2  30700  ballotlemimin  31372  ballotlemsdom  31378  ballotlemsel1i  31379  ballotlemsima  31382  ballotlemfrceq  31395  ballotlemfrcn0  31396  fsum2dsub  31487  reprgt  31501  breprexplemc  31512  erdszelem8  32047  cvmliftlem2  32135  cvmliftlem7  32140  supfz  32562  bcprod  32572  bccolsum  32573  poimirlem2  34438  poimirlem3  34439  poimirlem4  34440  poimirlem6  34442  poimirlem7  34443  poimirlem8  34444  poimirlem12  34448  poimirlem13  34449  poimirlem14  34450  poimirlem15  34451  poimirlem16  34452  poimirlem17  34453  poimirlem19  34455  poimirlem20  34456  poimirlem21  34457  poimirlem22  34458  poimirlem23  34459  poimirlem24  34460  poimirlem26  34462  poimirlem28  34464  poimirlem29  34465  poimirlem31  34467  poimirlem32  34468  mblfinlem2  34474  irrapxlem3  38919  irrapxlem4  38920  fzmaxdif  39076  jm2.23  39091  jm2.26lem3  39096  jm2.27dlem2  39105  binomcxplemnn0  40232  monoords  41118  elfzolem1  41143  fmul01lt1lem1  41420  fmul01lt1lem2  41421  sumnnodd  41466  dvnmul  41783  dvnprodlem1  41786  dvnprodlem2  41787  iblspltprt  41813  itgspltprt  41819  stoweidlem3  41844  stoweidlem17  41858  stoweidlem20  41861  stoweidlem26  41867  stoweidlem34  41875  fourierdlem11  41959  fourierdlem12  41960  fourierdlem15  41963  fourierdlem25  41973  fourierdlem41  41989  fourierdlem48  41995  fourierdlem49  41996  fourierdlem50  41997  fourierdlem52  41999  fourierdlem54  42001  fourierdlem79  42026  fourierdlem102  42049  fourierdlem114  42061  elaa2lem  42074  etransclem23  42098  etransclem28  42103  etransclem35  42110  etransclem38  42113  iundjiun  42298  2elfz2melfz  43048  elfzelfzlble  43051  iccpartgt  43083  fmtno4prm  43233  difmodm1lt  44077