Theorem elfzle1 13475

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ‘cfv 6493  (class class class)co 7361   ≤ cle 11174  ℤ_≥cuz 12782  ...cfz 13455

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7936  df-2nd 7937  df-neg 11374  df-z 12519  df-uz 12783  df-fz 13456

This theorem is referenced by:  elfz1eq  13483  fzdisj  13499  elfznn  13501  ssfzunsnext  13517  fznatpl1  13526  fznn0sub2  13583  fz0fzdiffz0  13585  difelfznle  13590  seqf1olem1  13997  seqf1olem2  13998  bcval4  14263  seqcoll  14420  seqcoll2  14421  fsum0diaglem  15732  mertenslem1  15843  fprodntriv  15901  fallfacval4  16002  divalglem6  16361  hashdvds  16739  prmdiveq  16750  4sqlem11  16920  4sqlem12  16921  dvfsumlem3  26008  birthdaylem3  26933  ppiltx  27157  ppiub  27184  lgsdilem2  27313  lgsquadlem1  27360  chtppilimlem1  27453  dchrvmasumiflem1  27481  pntrlog2bndlem5  27561  pntpbnd1  27566  pntpbnd2  27567  pntlemh  27579  pntlemj  27583  ostth2lem2  27614  axlowdimlem16  29043  fzto1st1  33181  smattr  33962  smatbl  33963  smatbr  33964  ballotlem2  34652  ballotlemsdom  34675  ballotlemsima  34679  ballotlemfrcn0  34693  ballotlem1ri  34698  breprexplemc  34795  subfacp1lem1  35380  subfacp1lem5  35385  inffz  35931  poimirlem2  37960  poimirlem6  37964  poimirlem7  37965  poimirlem8  37966  poimirlem11  37969  poimirlem15  37973  poimirlem16  37974  poimirlem17  37975  poimirlem19  37977  poimirlem20  37978  poimirlem22  37980  poimirlem24  37982  poimirlem29  37987  poimirlem31  37989  poimirlem32  37990  mblfinlem2  37996  fdc  38083  aks6d1c1  42572  aks6d1c5lem1  42592  sticksstones6  42607  sticksstones7  42608  sticksstones10  42611  sticksstones12a  42613  sticksstones12  42614  bcled  42634  bcle2d  42635  unitscyglem2  42652  unitscyglem4  42654  irrapxlem3  43273  acongrep  43429  fzmaxdif  43430  acongeq  43432  jm2.23  43445  jm2.26lem3  43450  jm2.27dlem2  43459  monoords  45751  fmul01lt1lem1  46035  fmul01lt1lem2  46036  sumnnodd  46081  limsupubuzlem  46161  dvnmul  46392  dvnprodlem1  46395  dvnprodlem2  46396  iblspltprt  46422  itgspltprt  46428  stoweidlem3  46452  stoweidlem11  46460  stoweidlem20  46469  stoweidlem26  46475  stoweidlem34  46483  wallispi2  46522  dirkeritg  46551  fourierdlem11  46567  fourierdlem12  46568  fourierdlem15  46571  fourierdlem41  46597  fourierdlem48  46603  fourierdlem49  46604  fourierdlem50  46605  fourierdlem52  46607  fourierdlem54  46609  fourierdlem79  46634  fourierdlem102  46657  fourierdlem103  46658  fourierdlem104  46659  fourierdlem114  46669  elaa2lem  46682  etransclem3  46686  etransclem4  46687  etransclem7  46690  etransclem10  46693  etransclem23  46706  etransclem24  46707  etransclem31  46714  etransclem32  46715  etransclem35  46718  etransclem41  46724  etransclem46  46729  caratheodorylem1  46975  iccpartgt  47902