Theorem elfzle1 12644

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

Syntax hints:   → wi 4   ∈ wcel 2164   class class class wbr 4875  ‘cfv 6127  (class class class)co 6910   ≤ cle 10399  ℤ_≥cuz 11975  ...cfz 12626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214  ax-cnex 10315  ax-resscn 10316

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-iun 4744  df-br 4876  df-opab 4938  df-mpt 4955  df-id 5252  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-fv 6135  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-1st 7433  df-2nd 7434  df-neg 10595  df-z 11712  df-uz 11976  df-fz 12627

This theorem is referenced by:  elfz1eq  12652  fzdisj  12668  elfznn  12670  ssfzunsnext  12686  fznatpl1  12695  fznn0sub2  12748  fz0fzdiffz0  12750  difelfznle  12755  seqf1olem1  13141  seqf1olem2  13142  bcval4  13394  seqcoll  13544  seqcoll2  13545  fsum0diaglem  14889  mertenslem1  14996  fprodntriv  15052  fallfacval4  15153  divalglem6  15502  hashdvds  15858  prmdiveq  15869  4sqlem11  16037  4sqlem12  16038  dvfsumlem3  24197  birthdaylem3  25100  ppiltx  25323  ppiub  25349  lgsdilem2  25478  lgsquadlem1  25525  chtppilimlem1  25582  dchrvmasumiflem1  25610  pntrlog2bndlem5  25690  pntpbnd1  25695  pntpbnd2  25696  pntlemh  25708  pntlemj  25712  ostth2lem2  25743  axlowdimlem16  26263  fzto1st1  30393  smattr  30406  smatbl  30407  smatbr  30408  ballotlem2  31092  ballotlemsdom  31115  ballotlemsima  31119  ballotlemfrcn0  31133  ballotlem1ri  31138  breprexplemc  31255  subfacp1lem1  31703  subfacp1lem5  31708  inffz  32153  poimirlem2  33954  poimirlem6  33958  poimirlem7  33959  poimirlem8  33960  poimirlem11  33963  poimirlem15  33967  poimirlem16  33968  poimirlem17  33969  poimirlem19  33971  poimirlem20  33972  poimirlem22  33974  poimirlem24  33976  poimirlem29  33981  poimirlem31  33983  poimirlem32  33984  mblfinlem2  33990  fdc  34082  irrapxlem3  38231  acongrep  38389  fzmaxdif  38390  acongeq  38392  jm2.23  38405  jm2.26lem3  38410  jm2.27dlem2  38419  monoords  40307  fmul01lt1lem1  40609  fmul01lt1lem2  40610  sumnnodd  40655  limsupubuzlem  40737  dvnmul  40951  dvnprodlem1  40954  dvnprodlem2  40955  iblspltprt  40981  itgspltprt  40987  stoweidlem3  41012  stoweidlem11  41020  stoweidlem20  41029  stoweidlem26  41035  stoweidlem34  41043  wallispi2  41082  dirkeritg  41111  fourierdlem11  41127  fourierdlem12  41128  fourierdlem15  41131  fourierdlem41  41157  fourierdlem48  41163  fourierdlem49  41164  fourierdlem50  41165  fourierdlem52  41167  fourierdlem54  41169  fourierdlem79  41194  fourierdlem102  41217  fourierdlem103  41218  fourierdlem104  41219  fourierdlem114  41229  elaa2lem  41242  etransclem3  41246  etransclem4  41247  etransclem7  41250  etransclem10  41253  etransclem23  41266  etransclem24  41267  etransclem31  41274  etransclem32  41275  etransclem35  41278  etransclem41  41284  etransclem46  41289  caratheodorylem1  41532  iccpartgt  42249