Theorem elfzle1 13587

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5166  ‘cfv 6573  (class class class)co 7448   ≤ cle 11325  ℤ_≥cuz 12903  ...cfz 13567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-neg 11523  df-z 12640  df-uz 12904  df-fz 13568

This theorem is referenced by:  elfz1eq  13595  fzdisj  13611  elfznn  13613  ssfzunsnext  13629  fznatpl1  13638  fznn0sub2  13692  fz0fzdiffz0  13694  difelfznle  13699  seqf1olem1  14092  seqf1olem2  14093  bcval4  14356  seqcoll  14513  seqcoll2  14514  fsum0diaglem  15824  mertenslem1  15932  fprodntriv  15990  fallfacval4  16091  divalglem6  16446  hashdvds  16822  prmdiveq  16833  4sqlem11  17002  4sqlem12  17003  dvfsumlem3  26089  birthdaylem3  27014  ppiltx  27238  ppiub  27266  lgsdilem2  27395  lgsquadlem1  27442  chtppilimlem1  27535  dchrvmasumiflem1  27563  pntrlog2bndlem5  27643  pntpbnd1  27648  pntpbnd2  27649  pntlemh  27661  pntlemj  27665  ostth2lem2  27696  axlowdimlem16  28990  fzto1st1  33095  smattr  33745  smatbl  33746  smatbr  33747  ballotlem2  34453  ballotlemsdom  34476  ballotlemsima  34480  ballotlemfrcn0  34494  ballotlem1ri  34499  breprexplemc  34609  subfacp1lem1  35147  subfacp1lem5  35152  inffz  35692  poimirlem2  37582  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem11  37591  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem24  37604  poimirlem29  37609  poimirlem31  37611  poimirlem32  37612  mblfinlem2  37618  fdc  37705  aks6d1c1  42073  aks6d1c5lem1  42093  sticksstones6  42108  sticksstones7  42109  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  bcled  42135  bcle2d  42136  unitscyglem2  42153  unitscyglem4  42155  metakunt15  42176  irrapxlem3  42780  acongrep  42937  fzmaxdif  42938  acongeq  42940  jm2.23  42953  jm2.26lem3  42958  jm2.27dlem2  42967  monoords  45212  fmul01lt1lem1  45505  fmul01lt1lem2  45506  sumnnodd  45551  limsupubuzlem  45633  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  iblspltprt  45894  itgspltprt  45900  stoweidlem3  45924  stoweidlem11  45932  stoweidlem20  45941  stoweidlem26  45947  stoweidlem34  45955  wallispi2  45994  dirkeritg  46023  fourierdlem11  46039  fourierdlem12  46040  fourierdlem15  46043  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem52  46079  fourierdlem54  46081  fourierdlem79  46106  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem114  46141  elaa2lem  46154  etransclem3  46158  etransclem4  46159  etransclem7  46162  etransclem10  46165  etransclem23  46178  etransclem24  46179  etransclem31  46186  etransclem32  46187  etransclem35  46190  etransclem41  46196  etransclem46  46201  caratheodorylem1  46447  iccpartgt  47301