Theorem elfzle1 13532

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

Syntax hints:   → wi 4   ∈ wcel 2142   class class class wbr 5100  ‘cfv 6521  (class class class)co 7396   ≤ cle 11217  ℤ_≥cuz 12839  ...cfz 13512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-1st 7970  df-2nd 7971  df-neg 11417  df-z 12569  df-uz 12840  df-fz 13513

This theorem is referenced by:  elfz1eq  13540  fzdisj  13556  elfznn  13558  ssfzunsnext  13574  fznatpl1  13583  fznn0sub2  13640  fz0fzdiffz0  13642  difelfznle  13647  seqf1olem1  14054  seqf1olem2  14055  bcval4  14320  seqcoll  14477  seqcoll2  14478  fsum0diaglem  15803  mertenslem1  15914  fprodntriv  15972  fallfacval4  16073  divalglem6  16432  hashdvds  16810  prmdiveq  16821  4sqlem11  16991  4sqlem12  16992  dvfsumlem3  26090  birthdaylem3  27018  ppiltx  27241  ppiub  27268  lgsdilem2  27397  lgsquadlem1  27444  chtppilimlem1  27537  dchrvmasumiflem1  27565  pntrlog2bndlem5  27645  pntpbnd1  27650  pntpbnd2  27651  pntlemh  27663  pntlemj  27667  ostth2lem2  27698  axlowdimlem16  29158  fzto1st1  33282  smattr  34096  smatbl  34097  smatbr  34098  ballotlem2  34786  ballotlemsdom  34809  ballotlemsima  34813  ballotlemfrcn0  34827  ballotlem1ri  34832  breprexplemc  34926  subfacp1lem1  35529  subfacp1lem5  35534  inffz  36080  poimirlem2  38121  poimirlem6  38125  poimirlem7  38126  poimirlem8  38127  poimirlem11  38130  poimirlem15  38134  poimirlem16  38135  poimirlem17  38136  poimirlem19  38138  poimirlem20  38139  poimirlem22  38141  poimirlem24  38143  poimirlem29  38148  poimirlem31  38150  poimirlem32  38151  mblfinlem2  38157  fdc  38244  aks6d1c1  42733  aks6d1c5lem1  42753  sticksstones6  42768  sticksstones7  42769  sticksstones10  42772  sticksstones12a  42774  sticksstones12  42775  bcled  42795  bcle2d  42796  unitscyglem2  42813  unitscyglem4  42815  irrapxlem3  43401  acongrep  43557  fzmaxdif  43558  acongeq  43560  jm2.23  43573  jm2.26lem3  43578  jm2.27dlem2  43587  monoords  45876  fmul01lt1lem1  46160  fmul01lt1lem2  46161  sumnnodd  46206  limsupubuzlem  46286  dvnmul  46517  dvnprodlem1  46520  dvnprodlem2  46521  iblspltprt  46547  itgspltprt  46553  stoweidlem3  46577  stoweidlem11  46585  stoweidlem20  46594  stoweidlem26  46600  stoweidlem34  46608  wallispi2  46647  dirkeritg  46676  fourierdlem11  46692  fourierdlem12  46693  fourierdlem15  46696  fourierdlem41  46722  fourierdlem48  46728  fourierdlem49  46729  fourierdlem50  46730  fourierdlem52  46732  fourierdlem54  46734  fourierdlem79  46759  fourierdlem102  46782  fourierdlem103  46783  fourierdlem104  46784  fourierdlem114  46794  elaa2lem  46807  etransclem3  46811  etransclem4  46812  etransclem7  46815  etransclem10  46818  etransclem23  46831  etransclem24  46832  etransclem31  46839  etransclem32  46840  etransclem35  46843  etransclem41  46849  etransclem46  46854  caratheodorylem1  47100  iccpartgt  48033