Theorem elfzle1 13582

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ‘cfv 6533  (class class class)co 7414   ≤ cle 11269  ℤ_≥cuz 12888  ...cfz 13562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737  ax-cnex 11181  ax-resscn 11182

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7987  df-2nd 7988  df-neg 11469  df-z 12617  df-uz 12889  df-fz 13563

This theorem is used by:  elfz1eq  13590  fzdisj  13607  elfznn  13609  ssfzunsnext  13625  fznatpl1  13634  fznn0sub2  13691  fz0fzdiffz0  13693  difelfznle  13698  seqf1olem1  14106  seqf1olem2  14107  bcval4  14372  seqcoll  14530  seqcoll2  14531  fsum0diaglem  15863  mertenslem1  15974  fprodntriv  16030  fallfacval4  16130  divalglem6  16489  hashdvds  16867  prmdiveq  16878  4sqlem11  17048  4sqlem12  17049  dvfsumlem3  26256  birthdaylem3  27191  ppiltx  27414  ppiub  27441  lgsdilem2  27570  lgsquadlem1  27617  chtppilimlem1  27710  dchrvmasumiflem1  27738  pntrlog2bndlem5  27818  pntpbnd1  27823  pntpbnd2  27824  pntlemh  27836  pntlemj  27840  ostth2lem2  27871  axlowdimlem16  29415  fzto1st1  33543  smattr  34310  smatbl  34311  smatbr  34312  ballotlem2  35001  ballotlemsdom  35024  ballotlemsima  35028  ballotlemfrcn0  35042  ballotlem1ri  35047  breprexplemc  35141  subfacp1lem1  35759  subfacp1lem5  35764  inffz  36310  poimirlem2  38372  poimirlem6  38376  poimirlem7  38377  poimirlem8  38378  poimirlem11  38381  poimirlem15  38385  poimirlem16  38386  poimirlem17  38387  poimirlem19  38389  poimirlem20  38390  poimirlem22  38392  poimirlem24  38394  poimirlem29  38399  poimirlem31  38401  poimirlem32  38402  mblfinlem2  38408  fdc  38496  aks6d1c1  42983  aks6d1c5lem1  43003  sticksstones6  43018  sticksstones7  43019  sticksstones10  43022  sticksstones12a  43024  sticksstones12  43025  bcled  43045  bcle2d  43046  unitscyglem2  43063  unitscyglem4  43065  irrapxlem3  43666  acongrep  43822  fzmaxdif  43823  acongeq  43825  jm2.23  43838  jm2.26lem3  43843  jm2.27dlem2  43852  monoords  46131  fmul01lt1lem1  46415  fmul01lt1lem2  46416  sumnnodd  46461  limsupubuzlem  46541  dvnmul  46772  dvnprodlem1  46775  dvnprodlem2  46776  iblspltprt  46802  itgspltprt  46808  stoweidlem3  46832  stoweidlem11  46840  stoweidlem20  46849  stoweidlem26  46855  stoweidlem34  46863  wallispi2  46902  dirkeritg  46931  fourierdlem11  46947  fourierdlem12  46948  fourierdlem15  46951  fourierdlem41  46977  fourierdlem48  46983  fourierdlem49  46984  fourierdlem50  46985  fourierdlem52  46987  fourierdlem54  46989  fourierdlem79  47014  fourierdlem102  47037  fourierdlem103  47038  fourierdlem104  47039  fourierdlem114  47049  elaa2lem  47062  etransclem3  47066  etransclem4  47067  etransclem7  47070  etransclem10  47073  etransclem23  47086  etransclem24  47087  etransclem31  47094  etransclem32  47095  etransclem35  47098  etransclem41  47104  etransclem46  47109  caratheodorylem1  47355  iccpartgt  48328