Theorem elfzle1 13455

Description: A member of a finite set of sequential integer is greater than or equal to the lower bound. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzle1	⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐾)

Proof of Theorem elfzle1

Step	Hyp	Ref	Expression
1		elfzuz 13448	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		eluzle 12776	. 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝐾)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝐾)

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  ‘cfv 6500  (class class class)co 7368   ≤ cle 11179  ℤ_≥cuz 12763  ...cfz 13435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944  df-neg 11379  df-z 12501  df-uz 12764  df-fz 13436

This theorem is referenced by:  elfz1eq  13463  fzdisj  13479  elfznn  13481  ssfzunsnext  13497  fznatpl1  13506  fznn0sub2  13563  fz0fzdiffz0  13565  difelfznle  13570  seqf1olem1  13976  seqf1olem2  13977  bcval4  14242  seqcoll  14399  seqcoll2  14400  fsum0diaglem  15711  mertenslem1  15819  fprodntriv  15877  fallfacval4  15978  divalglem6  16337  hashdvds  16714  prmdiveq  16725  4sqlem11  16895  4sqlem12  16896  dvfsumlem3  26003  birthdaylem3  26931  ppiltx  27155  ppiub  27183  lgsdilem2  27312  lgsquadlem1  27359  chtppilimlem1  27452  dchrvmasumiflem1  27480  pntrlog2bndlem5  27560  pntpbnd1  27565  pntpbnd2  27566  pntlemh  27578  pntlemj  27582  ostth2lem2  27613  axlowdimlem16  29042  fzto1st1  33196  smattr  33977  smatbl  33978  smatbr  33979  ballotlem2  34667  ballotlemsdom  34690  ballotlemsima  34694  ballotlemfrcn0  34708  ballotlem1ri  34713  breprexplemc  34810  subfacp1lem1  35395  subfacp1lem5  35400  inffz  35946  poimirlem2  37873  poimirlem6  37877  poimirlem7  37878  poimirlem8  37879  poimirlem11  37882  poimirlem15  37886  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem22  37893  poimirlem24  37895  poimirlem29  37900  poimirlem31  37902  poimirlem32  37903  mblfinlem2  37909  fdc  37996  aks6d1c1  42486  aks6d1c5lem1  42506  sticksstones6  42521  sticksstones7  42522  sticksstones10  42525  sticksstones12a  42527  sticksstones12  42528  bcled  42548  bcle2d  42549  unitscyglem2  42566  unitscyglem4  42568  irrapxlem3  43181  acongrep  43337  fzmaxdif  43338  acongeq  43340  jm2.23  43353  jm2.26lem3  43358  jm2.27dlem2  43367  monoords  45659  fmul01lt1lem1  45944  fmul01lt1lem2  45945  sumnnodd  45990  limsupubuzlem  46070  dvnmul  46301  dvnprodlem1  46304  dvnprodlem2  46305  iblspltprt  46331  itgspltprt  46337  stoweidlem3  46361  stoweidlem11  46369  stoweidlem20  46378  stoweidlem26  46384  stoweidlem34  46392  wallispi2  46431  dirkeritg  46460  fourierdlem11  46476  fourierdlem12  46477  fourierdlem15  46480  fourierdlem41  46506  fourierdlem48  46512  fourierdlem49  46513  fourierdlem50  46514  fourierdlem52  46516  fourierdlem54  46518  fourierdlem79  46543  fourierdlem102  46566  fourierdlem103  46567  fourierdlem104  46568  fourierdlem114  46578  elaa2lem  46591  etransclem3  46595  etransclem4  46596  etransclem7  46599  etransclem10  46602  etransclem23  46615  etransclem24  46616  etransclem31  46623  etransclem32  46624  etransclem35  46627  etransclem41  46633  etransclem46  46638  caratheodorylem1  46884  iccpartgt  47787