Theorem elfzle2 13465

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5102  ‘cfv 6499  (class class class)co 7369   ≤ cle 11185  ℤ_≥cuz 12769  ...cfz 13444

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-1st 7947  df-2nd 7948  df-neg 11384  df-z 12506  df-uz 12770  df-fz 13445

This theorem is referenced by:  elfz1eq  13472  fzdisj  13488  ssfzunsnext  13506  fznatpl1  13515  fzp1disj  13520  uzdisj  13534  fzneuz  13545  fznuz  13546  elfzmlbm  13575  difelfznle  13579  nn0disj  13581  elfzolem1  13641  seqf1olem1  13982  seqf1olem2  13983  bcval4  14248  bcp1nk  14258  hashf1  14398  seqcoll  14405  seqcoll2  14406  isercolllem2  15608  isercoll  15610  summolem2a  15657  fsum0diaglem  15718  mertenslem1  15826  prodmolem2a  15876  binomrisefac  15984  bpoly4  16001  fzm1ndvds  16268  prmind2  16631  prmdvdsfz  16651  isprm7  16654  hashdvds  16721  prmdiveq  16732  prmreclem3  16865  prmreclem5  16867  4sqlem11  16902  4sqlem12  16903  vdwlem1  16928  vdwlem3  16930  vdwlem6  16933  vdwlem9  16936  vdwlem10  16937  mndodconglem  19447  oddvds  19453  gexdvds  19490  coe1tmmul  22139  lebnumii  24841  ovolicc2lem4  25397  voliunlem1  25427  dvfsumle  25902  dvfsumleOLD  25903  dvfsumge  25904  dvfsumabs  25905  dvfsumlem3  25911  elply2  26077  coeeq2  26123  aaliou3lem6  26232  birthdaylem2  26838  birthdaylem3  26839  wilthlem1  26954  ftalem5  26963  basellem1  26967  basellem3  26969  ppiprm  27037  chtprm  27039  logfac2  27104  lgsval2lem  27194  lgsqrlem2  27234  lgseisenlem1  27262  lgseisenlem2  27263  lgseisenlem3  27264  lgsquadlem1  27267  lgsquadlem2  27268  2lgslem1a  27278  chebbnd1lem1  27356  dchrvmasumiflem1  27388  mulog2sumlem2  27422  pntrlog2bndlem6  27470  pntpbnd1  27473  pntpbnd2  27474  pntlemh  27486  pntlemj  27490  pntlemf  27492  axlowdimlem16  28860  crctcshwlkn0lem2  29714  crctcshlem4  29723  bcm1n  32691  psgnfzto1stlem  33030  cycpmco2lem6  33061  cycpmco2lem7  33062  smatrcl  33759  submateqlem1  33770  madjusmdetlem2  33791  ballotlemimin  34470  ballotlemsdom  34476  ballotlemsel1i  34477  ballotlemsima  34480  ballotlemfrceq  34493  ballotlemfrcn0  34494  fsum2dsub  34571  reprgt  34585  breprexplemc  34596  erdszelem8  35158  cvmliftlem2  35246  cvmliftlem7  35251  supfz  35689  bcprod  35698  bccolsum  35699  poimirlem2  37589  poimirlem3  37590  poimirlem4  37591  poimirlem6  37593  poimirlem7  37594  poimirlem8  37595  poimirlem12  37599  poimirlem13  37600  poimirlem14  37601  poimirlem15  37602  poimirlem16  37603  poimirlem17  37604  poimirlem19  37606  poimirlem20  37607  poimirlem21  37608  poimirlem22  37609  poimirlem23  37610  poimirlem24  37611  poimirlem26  37613  poimirlem28  37615  poimirlem29  37616  poimirlem31  37618  poimirlem32  37619  mblfinlem2  37625  aks4d1p5  42041  aks4d1p6  42042  aks4d1p8  42048  primrootlekpowne0  42066  aks6d1c1  42077  hashscontpow1  42082  aks6d1c5lem1  42097  sticksstones6  42112  sticksstones7  42113  sticksstones10  42116  sticksstones12a  42118  sticksstones12  42119  bcled  42139  bcle2d  42140  unitscyglem2  42157  unitscyglem4  42159  irrapxlem3  42785  irrapxlem4  42786  fzmaxdif  42943  jm2.23  42958  jm2.26lem3  42963  jm2.27dlem2  42972  binomcxplemnn0  44311  monoords  45268  fmul01lt1lem1  45555  fmul01lt1lem2  45556  sumnnodd  45601  dvnmul  45914  dvnprodlem1  45917  dvnprodlem2  45918  iblspltprt  45944  itgspltprt  45950  stoweidlem3  45974  stoweidlem17  45988  stoweidlem20  45991  stoweidlem26  45997  stoweidlem34  46005  fourierdlem11  46089  fourierdlem12  46090  fourierdlem15  46093  fourierdlem25  46103  fourierdlem41  46119  fourierdlem48  46125  fourierdlem49  46126  fourierdlem50  46127  fourierdlem52  46129  fourierdlem54  46131  fourierdlem79  46156  fourierdlem102  46179  fourierdlem114  46191  elaa2lem  46204  etransclem23  46228  etransclem28  46233  etransclem35  46240  etransclem38  46243  iundjiun  46431  2elfz2melfz  47292  elfzelfzlble  47295  iccpartgt  47401  fmtno4prm  47549