Theorem elfzle1 12905

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5030  ‘cfv 6324  (class class class)co 7135   ≤ cle 10665  ℤ_≥cuz 12231  ...cfz 12885

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-1st 7671  df-2nd 7672  df-neg 10862  df-z 11970  df-uz 12232  df-fz 12886

This theorem is referenced by:  elfz1eq  12913  fzdisj  12929  elfznn  12931  ssfzunsnext  12947  fznatpl1  12956  fznn0sub2  13009  fz0fzdiffz0  13011  difelfznle  13016  seqf1olem1  13405  seqf1olem2  13406  bcval4  13663  seqcoll  13818  seqcoll2  13819  fsum0diaglem  15123  mertenslem1  15232  fprodntriv  15288  fallfacval4  15389  divalglem6  15739  hashdvds  16102  prmdiveq  16113  4sqlem11  16281  4sqlem12  16282  dvfsumlem3  24631  birthdaylem3  25539  ppiltx  25762  ppiub  25788  lgsdilem2  25917  lgsquadlem1  25964  chtppilimlem1  26057  dchrvmasumiflem1  26085  pntrlog2bndlem5  26165  pntpbnd1  26170  pntpbnd2  26171  pntlemh  26183  pntlemj  26187  ostth2lem2  26218  axlowdimlem16  26751  fzto1st1  30794  smattr  31152  smatbl  31153  smatbr  31154  ballotlem2  31856  ballotlemsdom  31879  ballotlemsima  31883  ballotlemfrcn0  31897  ballotlem1ri  31902  breprexplemc  32013  subfacp1lem1  32539  subfacp1lem5  32544  inffz  33074  poimirlem2  35059  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem11  35068  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem22  35079  poimirlem24  35081  poimirlem29  35086  poimirlem31  35088  poimirlem32  35089  mblfinlem2  35095  fdc  35183  metakunt15  39364  irrapxlem3  39765  acongrep  39921  fzmaxdif  39922  acongeq  39924  jm2.23  39937  jm2.26lem3  39942  jm2.27dlem2  39951  monoords  41929  fmul01lt1lem1  42226  fmul01lt1lem2  42227  sumnnodd  42272  limsupubuzlem  42354  dvnmul  42585  dvnprodlem1  42588  dvnprodlem2  42589  iblspltprt  42615  itgspltprt  42621  stoweidlem3  42645  stoweidlem11  42653  stoweidlem20  42662  stoweidlem26  42668  stoweidlem34  42676  wallispi2  42715  dirkeritg  42744  fourierdlem11  42760  fourierdlem12  42761  fourierdlem15  42764  fourierdlem41  42790  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  fourierdlem52  42800  fourierdlem54  42802  fourierdlem79  42827  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem114  42862  elaa2lem  42875  etransclem3  42879  etransclem4  42880  etransclem7  42883  etransclem10  42886  etransclem23  42899  etransclem24  42900  etransclem31  42907  etransclem32  42908  etransclem35  42911  etransclem41  42917  etransclem46  42922  caratheodorylem1  43165  iccpartgt  43944