Theorem elfzle1 13670

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5105  ‘cfv 6546  (class class class)co 7427   ≤ cle 11354  ℤ_≥cuz 12975  ...cfz 13649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pr 5394  ax-un 7758  ax-cnex 11266  ax-resscn 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-fv 6554  df-ov 7430  df-oprab 7431  df-mpo 7432  df-1st 8008  df-2nd 8009  df-neg 11554  df-z 12704  df-uz 12976  df-fz 13650

This theorem is used by:  elfz1eq  13678  fzdisj  13695  elfznn  13697  ssfzunsnext  13713  fznatpl1  13722  fznn0sub2  13779  fz0fzdiffz0  13781  difelfznle  13786  seqf1olem1  14194  seqf1olem2  14195  bcval4  14461  seqcoll  14619  seqcoll2  14620  fsum0diaglem  15954  mertenslem1  16065  fprodntriv  16121  fallfacval4  16221  divalglem6  16580  hashdvds  16964  prmdiveq  16975  4sqlem11  17145  4sqlem12  17146  dvfsumlem3  26360  birthdaylem3  27293  ppiltx  27516  ppiub  27543  lgsdilem2  27672  lgsquadlem1  27719  chtppilimlem1  27812  dchrvmasumiflem1  27840  pntrlog2bndlem5  27920  pntpbnd1  27925  pntpbnd2  27926  pntlemh  27938  pntlemj  27942  ostth2lem2  27973  axlowdimlem16  29547  fzto1st1  33716  smattr  34484  smatbl  34485  smatbr  34486  ballotlem2  35174  ballotlemsdom  35197  ballotlemsima  35201  ballotlemfrcn0  35215  ballotlem1ri  35220  breprexplemc  35314  subfacp1lem1  36065  subfacp1lem5  36070  inffz  36622  poimirlem2  38680  poimirlem6  38684  poimirlem7  38685  poimirlem8  38686  poimirlem11  38689  poimirlem15  38693  poimirlem16  38694  poimirlem17  38695  poimirlem19  38697  poimirlem20  38698  poimirlem22  38700  poimirlem24  38702  poimirlem29  38707  poimirlem31  38709  poimirlem32  38710  mblfinlem2  38716  fdc  38819  aks6d1c1  43306  aks6d1c5lem1  43326  sticksstones6  43341  sticksstones7  43342  sticksstones10  43345  sticksstones12a  43347  sticksstones12  43348  bcled  43368  bcle2d  43369  unitscyglem2  43386  unitscyglem4  43388  irrapxlem3  43971  acongrep  44127  fzmaxdif  44128  acongeq  44130  jm2.23  44143  jm2.26lem3  44148  jm2.27dlem2  44157  monoords  46452  fmul01lt1lem1  46735  fmul01lt1lem2  46736  sumnnodd  46781  limsupubuzlem  46861  dvnmul  47092  dvnprodlem1  47095  dvnprodlem2  47096  iblspltprt  47122  itgspltprt  47128  stoweidlem3  47152  stoweidlem11  47160  stoweidlem20  47169  stoweidlem26  47175  stoweidlem34  47183  wallispi2  47222  dirkeritg  47251  fourierdlem11  47267  fourierdlem12  47268  fourierdlem15  47271  fourierdlem41  47297  fourierdlem48  47303  fourierdlem49  47304  fourierdlem50  47305  fourierdlem52  47307  fourierdlem54  47309  fourierdlem79  47334  fourierdlem102  47357  fourierdlem103  47358  fourierdlem104  47359  fourierdlem114  47369  elaa2lem  47382  etransclem3  47386  etransclem4  47387  etransclem7  47390  etransclem10  47393  etransclem23  47406  etransclem24  47407  etransclem31  47414  etransclem32  47415  etransclem35  47418  etransclem41  47424  etransclem46  47429  caratheodorylem1  47675  iccpartgt  48648