Theorem elfzle2 13509

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

Syntax hints:   → wi 4   ∈ wcel 2104   class class class wbr 5147  ‘cfv 6542  (class class class)co 7411   ≤ cle 11253  ℤ_≥cuz 12826  ...cfz 13488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-neg 11451  df-z 12563  df-uz 12827  df-fz 13489

This theorem is referenced by:  elfz1eq  13516  fzdisj  13532  ssfzunsnext  13550  fznatpl1  13559  fzp1disj  13564  uzdisj  13578  fzneuz  13586  fznuz  13587  elfzmlbm  13615  difelfznle  13619  nn0disj  13621  seqf1olem1  14011  seqf1olem2  14012  bcval4  14271  bcp1nk  14281  hashf1  14422  seqcoll  14429  seqcoll2  14430  isercolllem2  15616  isercoll  15618  summolem2a  15665  fsum0diaglem  15726  mertenslem1  15834  prodmolem2a  15882  binomrisefac  15990  bpoly4  16007  fzm1ndvds  16269  prmind2  16626  prmdvdsfz  16646  isprm7  16649  hashdvds  16712  prmdiveq  16723  prmreclem3  16855  prmreclem5  16857  4sqlem11  16892  4sqlem12  16893  vdwlem1  16918  vdwlem3  16920  vdwlem6  16923  vdwlem9  16926  vdwlem10  16927  mndodconglem  19450  oddvds  19456  gexdvds  19493  coe1tmmul  22019  lebnumii  24712  ovolicc2lem4  25269  voliunlem1  25299  dvfsumle  25773  dvfsumge  25774  dvfsumabs  25775  dvfsumlem3  25780  elply2  25945  coeeq2  25991  aaliou3lem6  26097  birthdaylem2  26693  birthdaylem3  26694  wilthlem1  26808  ftalem5  26817  basellem1  26821  basellem3  26823  ppiprm  26891  chtprm  26893  logfac2  26956  lgsval2lem  27046  lgsqrlem2  27086  lgseisenlem1  27114  lgseisenlem2  27115  lgseisenlem3  27116  lgsquadlem1  27119  lgsquadlem2  27120  2lgslem1a  27130  chebbnd1lem1  27208  dchrvmasumiflem1  27240  mulog2sumlem2  27274  pntrlog2bndlem6  27322  pntpbnd1  27325  pntpbnd2  27326  pntlemh  27338  pntlemj  27342  pntlemf  27344  axlowdimlem16  28482  crctcshwlkn0lem2  29332  crctcshlem4  29341  bcm1n  32273  psgnfzto1stlem  32529  cycpmco2lem6  32560  cycpmco2lem7  32561  smatrcl  33074  submateqlem1  33085  madjusmdetlem2  33106  ballotlemimin  33802  ballotlemsdom  33808  ballotlemsel1i  33809  ballotlemsima  33812  ballotlemfrceq  33825  ballotlemfrcn0  33826  fsum2dsub  33917  reprgt  33931  breprexplemc  33942  erdszelem8  34487  cvmliftlem2  34575  cvmliftlem7  34580  supfz  35002  bcprod  35012  bccolsum  35013  gg-dvfsumle  35468  poimirlem2  36793  poimirlem3  36794  poimirlem4  36795  poimirlem6  36797  poimirlem7  36798  poimirlem8  36799  poimirlem12  36803  poimirlem13  36804  poimirlem14  36805  poimirlem15  36806  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem21  36812  poimirlem22  36813  poimirlem23  36814  poimirlem24  36815  poimirlem26  36817  poimirlem28  36819  poimirlem29  36820  poimirlem31  36822  poimirlem32  36823  mblfinlem2  36829  aks4d1p5  41251  aks4d1p6  41252  aks4d1p8  41258  sticksstones6  41273  sticksstones7  41274  sticksstones10  41277  sticksstones12a  41279  sticksstones12  41280  metakunt1  41291  metakunt7  41297  metakunt15  41305  metakunt16  41306  metakunt22  41312  metakunt28  41318  metakunt30  41320  irrapxlem3  41864  irrapxlem4  41865  fzmaxdif  42022  jm2.23  42037  jm2.26lem3  42042  jm2.27dlem2  42051  binomcxplemnn0  43410  monoords  44305  elfzolem1  44329  fmul01lt1lem1  44598  fmul01lt1lem2  44599  sumnnodd  44644  dvnmul  44957  dvnprodlem1  44960  dvnprodlem2  44961  iblspltprt  44987  itgspltprt  44993  stoweidlem3  45017  stoweidlem17  45031  stoweidlem20  45034  stoweidlem26  45040  stoweidlem34  45048  fourierdlem11  45132  fourierdlem12  45133  fourierdlem15  45136  fourierdlem25  45146  fourierdlem41  45162  fourierdlem48  45168  fourierdlem49  45169  fourierdlem50  45170  fourierdlem52  45172  fourierdlem54  45174  fourierdlem79  45199  fourierdlem102  45222  fourierdlem114  45234  elaa2lem  45247  etransclem23  45271  etransclem28  45276  etransclem35  45283  etransclem38  45286  iundjiun  45474  2elfz2melfz  46324  elfzelfzlble  46327  iccpartgt  46393  fmtno4prm  46541  difmodm1lt  47295