Theorem elfzle2 13585

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ‘cfv 6533  (class class class)co 7414   ≤ cle 11271  ℤ_≥cuz 12890  ...cfz 13564

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737  ax-cnex 11183  ax-resscn 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7987  df-2nd 7988  df-neg 11471  df-z 12619  df-uz 12891  df-fz 13565

This theorem is used by:  elfz1eq  13592  fzdisj  13609  ssfzunsnext  13627  fznatpl1  13636  fzp1disj  13641  uzdisj  13655  fzneuz  13666  fznuz  13667  elfzmlbm  13696  difelfznle  13700  nn0disj  13702  elfzolem1  13763  seqf1olem1  14108  seqf1olem2  14109  bcval4  14374  bcp1nk  14384  hashf1  14525  seqcoll  14532  seqcoll2  14533  isercolllem2  15756  isercoll  15758  summolem2a  15804  fsum0diaglem  15865  mertenslem1  15976  prodmolem2a  16024  binomrisefac  16131  bpoly4  16148  fzm1ndvds  16415  prmind2  16778  prmdvdsfz  16799  isprm7  16802  hashdvds  16869  prmdiveq  16880  prmreclem3  17013  prmreclem5  17015  4sqlem11  17050  4sqlem12  17051  vdwlem1  17076  vdwlem3  17078  vdwlem6  17081  vdwlem9  17084  vdwlem10  17085  mndodconglem  19671  oddvds  19677  gexdvds  19714  coe1tmmul  22506  lebnumii  25197  ovolicc2lem4  25751  voliunlem1  25781  dvfsumle  26251  dvfsumge  26252  dvfsumabs  26253  dvfsumlem3  26258  elply2  26424  coeeq2  26471  aaliou3lem6  26587  birthdaylem2  27192  birthdaylem3  27193  wilthlem1  27307  ftalem5  27316  basellem1  27320  basellem3  27322  ppiprm  27390  chtprm  27392  logfac2  27456  lgsval2lem  27546  lgsqrlem2  27586  lgseisenlem1  27614  lgseisenlem2  27615  lgseisenlem3  27616  lgsquadlem1  27619  lgsquadlem2  27620  2lgslem1a  27630  chebbnd1lem1  27708  dchrvmasumiflem1  27740  mulog2sumlem2  27774  pntrlog2bndlem6  27822  pntpbnd1  27825  pntpbnd2  27826  pntlemh  27838  pntlemj  27842  pntlemf  27844  axlowdimlem16  29417  crctcshwlkn0lem2  30282  crctcshlem4  30291  bcm1n  33269  psgnfzto1stlem  33543  cycpmco2lem6  33574  cycpmco2lem7  33575  smatrcl  34309  submateqlem1  34320  madjusmdetlem2  34341  ballotlemimin  35020  ballotlemsdom  35026  ballotlemsel1i  35027  ballotlemsima  35030  ballotlemfrceq  35043  ballotlemfrcn0  35044  fsum2dsub  35118  reprgt  35132  breprexplemc  35143  erdszelem8  35780  cvmliftlem2  35868  cvmliftlem7  35873  supfz  36311  bcprod  36320  bccolsum  36321  poimirlem2  38374  poimirlem3  38375  poimirlem4  38376  poimirlem6  38378  poimirlem7  38379  poimirlem8  38380  poimirlem12  38384  poimirlem13  38385  poimirlem14  38386  poimirlem15  38387  poimirlem16  38388  poimirlem17  38389  poimirlem19  38391  poimirlem20  38392  poimirlem21  38393  poimirlem22  38394  poimirlem23  38395  poimirlem24  38396  poimirlem26  38398  poimirlem28  38400  poimirlem29  38401  poimirlem31  38403  poimirlem32  38404  mblfinlem2  38410  aks4d1p5  42949  aks4d1p6  42950  aks4d1p8  42956  primrootlekpowne0  42974  aks6d1c1  42985  hashscontpow1  42990  aks6d1c5lem1  43005  sticksstones6  43020  sticksstones7  43021  sticksstones10  43024  sticksstones12a  43026  sticksstones12  43027  bcled  43047  bcle2d  43048  unitscyglem2  43065  unitscyglem4  43067  irrapxlem3  43668  irrapxlem4  43669  fzmaxdif  43825  jm2.23  43840  jm2.26lem3  43845  jm2.27dlem2  43854  binomcxplemnn0  45176  monoords  46133  fmul01lt1lem1  46417  fmul01lt1lem2  46418  sumnnodd  46463  dvnmul  46774  dvnprodlem1  46777  dvnprodlem2  46778  iblspltprt  46804  itgspltprt  46810  stoweidlem3  46834  stoweidlem17  46848  stoweidlem20  46851  stoweidlem26  46857  stoweidlem34  46865  fourierdlem11  46949  fourierdlem12  46950  fourierdlem15  46953  fourierdlem25  46963  fourierdlem41  46979  fourierdlem48  46985  fourierdlem49  46986  fourierdlem50  46987  fourierdlem52  46989  fourierdlem54  46991  fourierdlem79  47016  fourierdlem102  47039  fourierdlem114  47051  elaa2lem  47064  etransclem23  47088  etransclem28  47093  etransclem35  47100  etransclem38  47103  iundjiun  47291  2elfz2melfz  48209  elfzelfzlble  48212  iccpartgt  48330  fmtno4prm  48481