Theorem elfzle2 13547

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

Syntax hints:   → wi 4   ∈ wcel 2145   class class class wbr 5105  ‘cfv 6525  (class class class)co 7400   ≤ cle 11232  ℤ_≥cuz 12853  ...cfz 13526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722  ax-cnex 11144  ax-resscn 11145

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-1st 7974  df-2nd 7975  df-neg 11432  df-z 12583  df-uz 12854  df-fz 13527

This theorem is referenced by:  elfz1eq  13554  fzdisj  13570  ssfzunsnext  13588  fznatpl1  13597  fzp1disj  13602  uzdisj  13616  fzneuz  13627  fznuz  13628  elfzmlbm  13657  difelfznle  13661  nn0disj  13663  elfzolem1  13724  seqf1olem1  14068  seqf1olem2  14069  bcval4  14334  bcp1nk  14344  hashf1  14484  seqcoll  14491  seqcoll2  14492  isercolllem2  15707  isercoll  15709  summolem2a  15756  fsum0diaglem  15817  mertenslem1  15928  prodmolem2a  15978  binomrisefac  16086  bpoly4  16103  fzm1ndvds  16370  prmind2  16733  prmdvdsfz  16754  isprm7  16757  hashdvds  16824  prmdiveq  16835  prmreclem3  16968  prmreclem5  16970  4sqlem11  17005  4sqlem12  17006  vdwlem1  17031  vdwlem3  17033  vdwlem6  17036  vdwlem9  17039  vdwlem10  17040  mndodconglem  19602  oddvds  19608  gexdvds  19645  coe1tmmul  22398  lebnumii  25086  ovolicc2lem4  25640  voliunlem1  25670  dvfsumle  26141  dvfsumge  26142  dvfsumabs  26143  dvfsumlem3  26148  elply2  26314  coeeq2  26360  aaliou3lem6  26470  birthdaylem2  27075  birthdaylem3  27076  wilthlem1  27190  ftalem5  27199  basellem1  27203  basellem3  27205  ppiprm  27273  chtprm  27275  logfac2  27339  lgsval2lem  27429  lgsqrlem2  27469  lgseisenlem1  27497  lgseisenlem2  27498  lgseisenlem3  27499  lgsquadlem1  27502  lgsquadlem2  27503  2lgslem1a  27513  chebbnd1lem1  27591  dchrvmasumiflem1  27623  mulog2sumlem2  27657  pntrlog2bndlem6  27705  pntpbnd1  27708  pntpbnd2  27709  pntlemh  27721  pntlemj  27725  pntlemf  27727  axlowdimlem16  29216  crctcshwlkn0lem2  30069  crctcshlem4  30078  bcm1n  33052  psgnfzto1stlem  33333  cycpmco2lem6  33364  cycpmco2lem7  33365  smatrcl  34103  submateqlem1  34114  madjusmdetlem2  34135  ballotlemimin  34813  ballotlemsdom  34819  ballotlemsel1i  34820  ballotlemsima  34823  ballotlemfrceq  34836  ballotlemfrcn0  34837  fsum2dsub  34911  reprgt  34925  breprexplemc  34936  erdszelem8  35561  cvmliftlem2  35649  cvmliftlem7  35654  supfz  36092  bcprod  36101  bccolsum  36102  poimirlem2  38133  poimirlem3  38134  poimirlem4  38135  poimirlem6  38137  poimirlem7  38138  poimirlem8  38139  poimirlem12  38143  poimirlem13  38144  poimirlem14  38145  poimirlem15  38146  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem20  38151  poimirlem21  38152  poimirlem22  38153  poimirlem23  38154  poimirlem24  38155  poimirlem26  38157  poimirlem28  38159  poimirlem29  38160  poimirlem31  38162  poimirlem32  38163  mblfinlem2  38169  aks4d1p5  42709  aks4d1p6  42710  aks4d1p8  42716  primrootlekpowne0  42734  aks6d1c1  42745  hashscontpow1  42750  aks6d1c5lem1  42765  sticksstones6  42780  sticksstones7  42781  sticksstones10  42784  sticksstones12a  42786  sticksstones12  42787  bcled  42807  bcle2d  42808  unitscyglem2  42825  unitscyglem4  42827  irrapxlem3  43413  irrapxlem4  43414  fzmaxdif  43570  jm2.23  43585  jm2.26lem3  43590  jm2.27dlem2  43599  binomcxplemnn0  44923  monoords  45874  fmul01lt1lem1  46158  fmul01lt1lem2  46159  sumnnodd  46204  dvnmul  46515  dvnprodlem1  46518  dvnprodlem2  46519  iblspltprt  46545  itgspltprt  46551  stoweidlem3  46575  stoweidlem17  46589  stoweidlem20  46592  stoweidlem26  46598  stoweidlem34  46606  fourierdlem11  46690  fourierdlem12  46691  fourierdlem15  46694  fourierdlem25  46704  fourierdlem41  46720  fourierdlem48  46726  fourierdlem49  46727  fourierdlem50  46728  fourierdlem52  46730  fourierdlem54  46732  fourierdlem79  46757  fourierdlem102  46780  fourierdlem114  46792  elaa2lem  46805  etransclem23  46829  etransclem28  46834  etransclem35  46841  etransclem38  46844  iundjiun  47032  2elfz2melfz  47910  elfzelfzlble  47913  iccpartgt  48031  fmtno4prm  48182