Theorem elfzle2 13588

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5166  ‘cfv 6573  (class class class)co 7448   ≤ cle 11325  ℤ_≥cuz 12903  ...cfz 13567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-neg 11523  df-z 12640  df-uz 12904  df-fz 13568

This theorem is referenced by:  elfz1eq  13595  fzdisj  13611  ssfzunsnext  13629  fznatpl1  13638  fzp1disj  13643  uzdisj  13657  fzneuz  13665  fznuz  13666  elfzmlbm  13695  difelfznle  13699  nn0disj  13701  seqf1olem1  14092  seqf1olem2  14093  bcval4  14356  bcp1nk  14366  hashf1  14506  seqcoll  14513  seqcoll2  14514  isercolllem2  15714  isercoll  15716  summolem2a  15763  fsum0diaglem  15824  mertenslem1  15932  prodmolem2a  15982  binomrisefac  16090  bpoly4  16107  fzm1ndvds  16370  prmind2  16732  prmdvdsfz  16752  isprm7  16755  hashdvds  16822  prmdiveq  16833  prmreclem3  16965  prmreclem5  16967  4sqlem11  17002  4sqlem12  17003  vdwlem1  17028  vdwlem3  17030  vdwlem6  17033  vdwlem9  17036  vdwlem10  17037  mndodconglem  19583  oddvds  19589  gexdvds  19626  coe1tmmul  22301  lebnumii  25017  ovolicc2lem4  25574  voliunlem1  25604  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvfsumabs  26083  dvfsumlem3  26089  elply2  26255  coeeq2  26301  aaliou3lem6  26408  birthdaylem2  27013  birthdaylem3  27014  wilthlem1  27129  ftalem5  27138  basellem1  27142  basellem3  27144  ppiprm  27212  chtprm  27214  logfac2  27279  lgsval2lem  27369  lgsqrlem2  27409  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgsquadlem1  27442  lgsquadlem2  27443  2lgslem1a  27453  chebbnd1lem1  27531  dchrvmasumiflem1  27563  mulog2sumlem2  27597  pntrlog2bndlem6  27645  pntpbnd1  27648  pntpbnd2  27649  pntlemh  27661  pntlemj  27665  pntlemf  27667  axlowdimlem16  28990  crctcshwlkn0lem2  29844  crctcshlem4  29853  bcm1n  32800  psgnfzto1stlem  33093  cycpmco2lem6  33124  cycpmco2lem7  33125  smatrcl  33742  submateqlem1  33753  madjusmdetlem2  33774  ballotlemimin  34470  ballotlemsdom  34476  ballotlemsel1i  34477  ballotlemsima  34480  ballotlemfrceq  34493  ballotlemfrcn0  34494  fsum2dsub  34584  reprgt  34598  breprexplemc  34609  erdszelem8  35166  cvmliftlem2  35254  cvmliftlem7  35259  supfz  35691  bcprod  35700  bccolsum  35701  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem12  37592  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem26  37606  poimirlem28  37608  poimirlem29  37609  poimirlem31  37611  poimirlem32  37612  mblfinlem2  37618  aks4d1p5  42037  aks4d1p6  42038  aks4d1p8  42044  primrootlekpowne0  42062  aks6d1c1  42073  hashscontpow1  42078  aks6d1c5lem1  42093  sticksstones6  42108  sticksstones7  42109  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  bcled  42135  bcle2d  42136  unitscyglem2  42153  unitscyglem4  42155  metakunt1  42162  metakunt7  42168  metakunt15  42176  metakunt16  42177  metakunt22  42183  metakunt28  42189  metakunt30  42191  irrapxlem3  42780  irrapxlem4  42781  fzmaxdif  42938  jm2.23  42953  jm2.26lem3  42958  jm2.27dlem2  42967  binomcxplemnn0  44318  monoords  45212  elfzolem1  45236  fmul01lt1lem1  45505  fmul01lt1lem2  45506  sumnnodd  45551  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  iblspltprt  45894  itgspltprt  45900  stoweidlem3  45924  stoweidlem17  45938  stoweidlem20  45941  stoweidlem26  45947  stoweidlem34  45955  fourierdlem11  46039  fourierdlem12  46040  fourierdlem15  46043  fourierdlem25  46053  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem52  46079  fourierdlem54  46081  fourierdlem79  46106  fourierdlem102  46129  fourierdlem114  46141  elaa2lem  46154  etransclem23  46178  etransclem28  46183  etransclem35  46190  etransclem38  46193  iundjiun  46381  2elfz2melfz  47233  elfzelfzlble  47236  iccpartgt  47301  fmtno4prm  47449  difmodm1lt  48256