Theorem elfzle2 12912

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5066  ‘cfv 6355  (class class class)co 7156   ≤ cle 10676  ℤ_≥cuz 12244  ...cfz 12893

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-1st 7689  df-2nd 7690  df-neg 10873  df-z 11983  df-uz 12245  df-fz 12894

This theorem is referenced by:  elfz1eq  12919  fzdisj  12935  ssfzunsnext  12953  fznatpl1  12962  fzp1disj  12967  uzdisj  12981  fzneuz  12989  fznuz  12990  elfzmlbm  13018  difelfznle  13022  nn0disj  13024  seqf1olem1  13410  seqf1olem2  13411  bcval4  13668  bcp1nk  13678  hashf1  13816  seqcoll  13823  seqcoll2  13824  isercolllem2  15022  isercoll  15024  summolem2a  15072  fsum0diaglem  15131  mertenslem1  15240  prodmolem2a  15288  binomrisefac  15396  bpoly4  15413  fzm1ndvds  15672  prmind2  16029  prmdvdsfz  16049  isprm7  16052  hashdvds  16112  prmdiveq  16123  prmreclem3  16254  prmreclem5  16256  4sqlem11  16291  4sqlem12  16292  vdwlem1  16317  vdwlem3  16319  vdwlem6  16322  vdwlem9  16325  vdwlem10  16326  mndodconglem  18669  oddvds  18675  gexdvds  18709  coe1tmmul  20445  lebnumii  23570  ovolicc2lem4  24121  voliunlem1  24151  dvfsumle  24618  dvfsumge  24619  dvfsumabs  24620  dvfsumlem3  24625  elply2  24786  coeeq2  24832  aaliou3lem6  24937  birthdaylem2  25530  birthdaylem3  25531  wilthlem1  25645  ftalem5  25654  basellem1  25658  basellem3  25660  ppiprm  25728  chtprm  25730  logfac2  25793  lgsval2lem  25883  lgsqrlem2  25923  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgsquadlem1  25956  lgsquadlem2  25957  2lgslem1a  25967  chebbnd1lem1  26045  dchrvmasumiflem1  26077  mulog2sumlem2  26111  pntrlog2bndlem6  26159  pntpbnd1  26162  pntpbnd2  26163  pntlemh  26175  pntlemj  26179  pntlemf  26181  axlowdimlem16  26743  crctcshwlkn0lem2  27589  crctcshlem4  27598  bcm1n  30518  psgnfzto1stlem  30742  cycpmco2lem6  30773  cycpmco2lem7  30774  smatrcl  31061  submateqlem1  31072  madjusmdetlem2  31093  ballotlemimin  31763  ballotlemsdom  31769  ballotlemsel1i  31770  ballotlemsima  31773  ballotlemfrceq  31786  ballotlemfrcn0  31787  fsum2dsub  31878  reprgt  31892  breprexplemc  31903  erdszelem8  32445  cvmliftlem2  32533  cvmliftlem7  32538  supfz  32960  bcprod  32970  bccolsum  32971  poimirlem2  34909  poimirlem3  34910  poimirlem4  34911  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem12  34919  poimirlem13  34920  poimirlem14  34921  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  poimirlem26  34933  poimirlem28  34935  poimirlem29  34936  poimirlem31  34938  poimirlem32  34939  mblfinlem2  34945  irrapxlem3  39470  irrapxlem4  39471  fzmaxdif  39627  jm2.23  39642  jm2.26lem3  39647  jm2.27dlem2  39656  binomcxplemnn0  40730  monoords  41613  elfzolem1  41638  fmul01lt1lem1  41914  fmul01lt1lem2  41915  sumnnodd  41960  dvnmul  42277  dvnprodlem1  42280  dvnprodlem2  42281  iblspltprt  42307  itgspltprt  42313  stoweidlem3  42337  stoweidlem17  42351  stoweidlem20  42354  stoweidlem26  42360  stoweidlem34  42368  fourierdlem11  42452  fourierdlem12  42453  fourierdlem15  42456  fourierdlem25  42466  fourierdlem41  42482  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem52  42492  fourierdlem54  42494  fourierdlem79  42519  fourierdlem102  42542  fourierdlem114  42554  elaa2lem  42567  etransclem23  42591  etransclem28  42596  etransclem35  42603  etransclem38  42606  iundjiun  42791  2elfz2melfz  43567  elfzelfzlble  43570  iccpartgt  43636  fmtno4prm  43786  difmodm1lt  44631