Theorem elfzle2 13701

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   class class class wbr 5108  ‘cfv 6566  (class class class)co 7451   ≤ cle 11383  ℤ_≥cuz 13005  ...cfz 13679

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-cnex 11295  ax-resscn 11296

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-1st 8035  df-2nd 8036  df-neg 11583  df-z 12734  df-uz 13006  df-fz 13680

This theorem is used by:  elfz1eq  13708  fzdisj  13725  ssfzunsnext  13743  fznatpl1  13752  fzp1disj  13757  uzdisj  13771  fzneuz  13782  fznuz  13783  elfzmlbm  13812  difelfznle  13816  nn0disj  13818  elfzolem1  13879  seqf1olem1  14224  seqf1olem2  14225  bcval4  14492  bcp1nk  14502  hashf1  14643  seqcoll  14650  seqcoll2  14651  isercolllem2  15877  isercoll  15879  summolem2a  15925  fsum0diaglem  15986  mertenslem1  16097  prodmolem2a  16145  binomrisefac  16252  bpoly4  16269  fzm1ndvds  16536  prmind2  16904  prmdvdsfz  16925  isprm7  16928  hashdvds  16996  prmdiveq  17007  prmreclem3  17140  prmreclem5  17142  4sqlem11  17177  4sqlem12  17178  vdwlem1  17203  vdwlem3  17205  vdwlem6  17208  vdwlem9  17211  vdwlem10  17212  mndodconglem  19806  oddvds  19812  gexdvds  19849  coe1tmmul  22651  lebnumii  25342  ovolicc2lem4  25896  voliunlem1  25926  dvfsumle  26396  dvfsumge  26397  dvfsumabs  26398  dvfsumlem3  26403  elply2  26569  coeeq2  26616  aaliou3lem6  26732  birthdaylem2  27337  birthdaylem3  27338  wilthlem1  27452  ftalem5  27461  basellem1  27465  basellem3  27467  ppiprm  27535  chtprm  27537  logfac2  27601  lgsval2lem  27691  lgsqrlem2  27731  lgseisenlem1  27759  lgseisenlem2  27760  lgseisenlem3  27761  lgsquadlem1  27764  lgsquadlem2  27765  2lgslem1a  27775  chebbnd1lem1  27853  dchrvmasumiflem1  27885  mulog2sumlem2  27919  pntrlog2bndlem6  27967  pntpbnd1  27970  pntpbnd2  27971  pntlemh  27983  pntlemj  27987  pntlemf  27989  axlowdimlem16  29592  crctcshwlkn0lem2  30457  crctcshlem4  30466  bcm1n  33483  psgnfzto1stlem  33760  cycpmco2lem6  33791  cycpmco2lem7  33792  smatrcl  34539  submateqlem1  34550  madjusmdetlem2  34571  ballotlemimin  35249  ballotlemsdom  35255  ballotlemsel1i  35256  ballotlemsima  35259  ballotlemfrceq  35272  ballotlemfrcn0  35273  fsum2dsub  35347  reprgt  35361  breprexplemc  35372  erdszelem8  36171  cvmliftlem2  36259  cvmliftlem7  36264  supfz  36709  bcprod  36718  bccolsum  36719  poimirlem2  38808  poimirlem3  38809  poimirlem4  38810  poimirlem6  38812  poimirlem7  38813  poimirlem8  38814  poimirlem12  38818  poimirlem13  38819  poimirlem14  38820  poimirlem15  38821  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem21  38827  poimirlem22  38828  poimirlem23  38829  poimirlem24  38830  poimirlem26  38832  poimirlem28  38834  poimirlem29  38835  poimirlem31  38837  poimirlem32  38838  mblfinlem2  38844  aks4d1p5  43396  aks4d1p6  43397  aks4d1p8  43403  primrootlekpowne0  43421  aks6d1c1  43432  hashscontpow1  43437  aks6d1c5lem1  43452  sticksstones6  43467  sticksstones7  43468  sticksstones10  43471  sticksstones12a  43473  sticksstones12  43474  bcled  43494  bcle2d  43495  unitscyglem2  43512  unitscyglem4  43514  irrapxlem3  44097  irrapxlem4  44098  fzmaxdif  44254  jm2.23  44269  jm2.26lem3  44274  jm2.27dlem2  44283  binomcxplemnn0  45594  monoords  46586  fmul01lt1lem1  46869  fmul01lt1lem2  46870  sumnnodd  46915  dvnmul  47226  dvnprodlem1  47229  dvnprodlem2  47230  iblspltprt  47256  itgspltprt  47262  stoweidlem3  47286  stoweidlem17  47300  stoweidlem20  47303  stoweidlem26  47309  stoweidlem34  47317  fourierdlem11  47401  fourierdlem12  47402  fourierdlem15  47405  fourierdlem25  47415  fourierdlem41  47431  fourierdlem48  47437  fourierdlem49  47438  fourierdlem50  47439  fourierdlem52  47441  fourierdlem54  47443  fourierdlem79  47468  fourierdlem102  47491  fourierdlem114  47503  elaa2lem  47516  etransclem23  47540  etransclem28  47545  etransclem35  47552  etransclem38  47555  iundjiun  47743  2elfz2melfz  48661  elfzelfzlble  48664  iccpartgt  48782  fmtno4prm  48933