Theorem elfzle1 13204

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5075  ‘cfv 6423  (class class class)co 7260   ≤ cle 10957  ℤ_≥cuz 12527  ...cfz 13184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7571  ax-cnex 10874  ax-resscn 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3429  df-sbc 3717  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-iun 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5485  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-iota 6381  df-fun 6425  df-fn 6426  df-f 6427  df-fv 6431  df-ov 7263  df-oprab 7264  df-mpo 7265  df-1st 7809  df-2nd 7810  df-neg 11154  df-z 12266  df-uz 12528  df-fz 13185

This theorem is referenced by:  elfz1eq  13212  fzdisj  13228  elfznn  13230  ssfzunsnext  13246  fznatpl1  13255  fznn0sub2  13308  fz0fzdiffz0  13310  difelfznle  13315  seqf1olem1  13706  seqf1olem2  13707  bcval4  13965  seqcoll  14122  seqcoll2  14123  fsum0diaglem  15432  mertenslem1  15540  fprodntriv  15596  fallfacval4  15697  divalglem6  16051  hashdvds  16420  prmdiveq  16431  4sqlem11  16600  4sqlem12  16601  dvfsumlem3  25135  birthdaylem3  26046  ppiltx  26269  ppiub  26295  lgsdilem2  26424  lgsquadlem1  26471  chtppilimlem1  26564  dchrvmasumiflem1  26592  pntrlog2bndlem5  26672  pntpbnd1  26677  pntpbnd2  26678  pntlemh  26690  pntlemj  26694  ostth2lem2  26725  axlowdimlem16  27268  fzto1st1  31311  smattr  31691  smatbl  31692  smatbr  31693  ballotlem2  32397  ballotlemsdom  32420  ballotlemsima  32424  ballotlemfrcn0  32438  ballotlem1ri  32443  breprexplemc  32554  subfacp1lem1  33083  subfacp1lem5  33088  inffz  33643  poimirlem2  35748  poimirlem6  35752  poimirlem7  35753  poimirlem8  35754  poimirlem11  35757  poimirlem15  35761  poimirlem16  35762  poimirlem17  35763  poimirlem19  35765  poimirlem20  35766  poimirlem22  35768  poimirlem24  35770  poimirlem29  35775  poimirlem31  35777  poimirlem32  35778  mblfinlem2  35784  fdc  35872  sticksstones6  40077  sticksstones7  40078  sticksstones10  40081  sticksstones12a  40083  sticksstones12  40084  metakunt15  40109  irrapxlem3  40604  acongrep  40760  fzmaxdif  40761  acongeq  40763  jm2.23  40776  jm2.26lem3  40781  jm2.27dlem2  40790  monoords  42768  fmul01lt1lem1  43057  fmul01lt1lem2  43058  sumnnodd  43103  limsupubuzlem  43185  dvnmul  43416  dvnprodlem1  43419  dvnprodlem2  43420  iblspltprt  43446  itgspltprt  43452  stoweidlem3  43476  stoweidlem11  43484  stoweidlem20  43493  stoweidlem26  43499  stoweidlem34  43507  wallispi2  43546  dirkeritg  43575  fourierdlem11  43591  fourierdlem12  43592  fourierdlem15  43595  fourierdlem41  43621  fourierdlem48  43627  fourierdlem49  43628  fourierdlem50  43629  fourierdlem52  43631  fourierdlem54  43633  fourierdlem79  43658  fourierdlem102  43681  fourierdlem103  43682  fourierdlem104  43683  fourierdlem114  43693  elaa2lem  43706  etransclem3  43710  etransclem4  43711  etransclem7  43714  etransclem10  43717  etransclem23  43730  etransclem24  43731  etransclem31  43738  etransclem32  43739  etransclem35  43742  etransclem41  43748  etransclem46  43753  caratheodorylem1  43996  iccpartgt  44809