Theorem elfzle2 13551

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

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5109  ‘cfv 6536  (class class class)co 7410   ≤ cle 11239  ℤ_≥cuz 12857  ...cfz 13530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7982  df-2nd 7983  df-neg 11439  df-z 12587  df-uz 12858  df-fz 13531

This theorem is referenced by:  elfz1eq  13558  fzdisj  13575  ssfzunsnext  13593  fznatpl1  13602  fzp1disj  13607  uzdisj  13621  fzneuz  13632  fznuz  13633  elfzmlbm  13662  difelfznle  13666  nn0disj  13668  elfzolem1  13729  seqf1olem1  14073  seqf1olem2  14074  bcval4  14339  bcp1nk  14349  hashf1  14490  seqcoll  14497  seqcoll2  14498  isercolllem2  15713  isercoll  15715  summolem2a  15762  fsum0diaglem  15823  mertenslem1  15934  prodmolem2a  15984  binomrisefac  16091  bpoly4  16108  fzm1ndvds  16375  prmind2  16738  prmdvdsfz  16759  isprm7  16762  hashdvds  16829  prmdiveq  16840  prmreclem3  16973  prmreclem5  16975  4sqlem11  17010  4sqlem12  17011  vdwlem1  17036  vdwlem3  17038  vdwlem6  17041  vdwlem9  17044  vdwlem10  17045  mndodconglem  19606  oddvds  19612  gexdvds  19649  coe1tmmul  22438  lebnumii  25125  ovolicc2lem4  25679  voliunlem1  25709  dvfsumle  26180  dvfsumge  26181  dvfsumabs  26182  dvfsumlem3  26187  elply2  26353  coeeq2  26399  aaliou3lem6  26511  birthdaylem2  27117  birthdaylem3  27118  wilthlem1  27232  ftalem5  27241  basellem1  27245  basellem3  27247  ppiprm  27315  chtprm  27317  logfac2  27381  lgsval2lem  27471  lgsqrlem2  27511  lgseisenlem1  27539  lgseisenlem2  27540  lgseisenlem3  27541  lgsquadlem1  27544  lgsquadlem2  27545  2lgslem1a  27555  chebbnd1lem1  27633  dchrvmasumiflem1  27665  mulog2sumlem2  27699  pntrlog2bndlem6  27747  pntpbnd1  27750  pntpbnd2  27751  pntlemh  27763  pntlemj  27767  pntlemf  27769  axlowdimlem16  29307  crctcshwlkn0lem2  30160  crctcshlem4  30169  bcm1n  33140  psgnfzto1stlem  33420  cycpmco2lem6  33451  cycpmco2lem7  33452  smatrcl  34186  submateqlem1  34197  madjusmdetlem2  34218  ballotlemimin  34896  ballotlemsdom  34902  ballotlemsel1i  34903  ballotlemsima  34906  ballotlemfrceq  34919  ballotlemfrcn0  34920  fsum2dsub  34994  reprgt  35008  breprexplemc  35019  erdszelem8  35690  cvmliftlem2  35778  cvmliftlem7  35783  supfz  36221  bcprod  36230  bccolsum  36231  poimirlem2  38293  poimirlem3  38294  poimirlem4  38295  poimirlem6  38297  poimirlem7  38298  poimirlem8  38299  poimirlem12  38303  poimirlem13  38304  poimirlem14  38305  poimirlem15  38306  poimirlem16  38307  poimirlem17  38308  poimirlem19  38310  poimirlem20  38311  poimirlem21  38312  poimirlem22  38313  poimirlem23  38314  poimirlem24  38315  poimirlem26  38317  poimirlem28  38319  poimirlem29  38320  poimirlem31  38322  poimirlem32  38323  mblfinlem2  38329  aks4d1p5  42867  aks4d1p6  42868  aks4d1p8  42874  primrootlekpowne0  42892  aks6d1c1  42903  hashscontpow1  42908  aks6d1c5lem1  42923  sticksstones6  42938  sticksstones7  42939  sticksstones10  42942  sticksstones12a  42944  sticksstones12  42945  bcled  42965  bcle2d  42966  unitscyglem2  42983  unitscyglem4  42985  irrapxlem3  43571  irrapxlem4  43572  fzmaxdif  43728  jm2.23  43743  jm2.26lem3  43748  jm2.27dlem2  43757  binomcxplemnn0  45079  monoords  46036  fmul01lt1lem1  46320  fmul01lt1lem2  46321  sumnnodd  46366  dvnmul  46677  dvnprodlem1  46680  dvnprodlem2  46681  iblspltprt  46707  itgspltprt  46713  stoweidlem3  46737  stoweidlem17  46751  stoweidlem20  46754  stoweidlem26  46760  stoweidlem34  46768  fourierdlem11  46852  fourierdlem12  46853  fourierdlem15  46856  fourierdlem25  46866  fourierdlem41  46882  fourierdlem48  46888  fourierdlem49  46889  fourierdlem50  46890  fourierdlem52  46892  fourierdlem54  46894  fourierdlem79  46919  fourierdlem102  46942  fourierdlem114  46954  elaa2lem  46967  etransclem23  46991  etransclem28  46996  etransclem35  47003  etransclem38  47006  iundjiun  47194  2elfz2melfz  48075  elfzelfzlble  48078  iccpartgt  48196  fmtno4prm  48347