Theorem elfzle1 13554

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

Syntax hints:   → wi 4   ∈ wcel 2149   class class class wbr 5113  ‘cfv 6537  (class class class)co 7411   ≤ cle 11243  ℤ_≥cuz 12861  ...cfz 13534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733  ax-cnex 11155  ax-resscn 11156

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7985  df-2nd 7986  df-neg 11443  df-z 12591  df-uz 12862  df-fz 13535

This theorem is referenced by:  elfz1eq  13562  fzdisj  13578  elfznn  13580  ssfzunsnext  13596  fznatpl1  13605  fznn0sub2  13662  fz0fzdiffz0  13664  difelfznle  13669  seqf1olem1  14076  seqf1olem2  14077  bcval4  14342  seqcoll  14500  seqcoll2  14501  fsum0diaglem  15826  mertenslem1  15937  fprodntriv  15995  fallfacval4  16096  divalglem6  16455  hashdvds  16833  prmdiveq  16844  4sqlem11  17014  4sqlem12  17015  dvfsumlem3  26155  birthdaylem3  27083  ppiltx  27306  ppiub  27333  lgsdilem2  27462  lgsquadlem1  27509  chtppilimlem1  27602  dchrvmasumiflem1  27630  pntrlog2bndlem5  27710  pntpbnd1  27715  pntpbnd2  27716  pntlemh  27728  pntlemj  27732  ostth2lem2  27763  axlowdimlem16  29247  fzto1st1  33362  smattr  34133  smatbl  34134  smatbr  34135  ballotlem2  34823  ballotlemsdom  34846  ballotlemsima  34850  ballotlemfrcn0  34864  ballotlem1ri  34869  breprexplemc  34963  subfacp1lem1  35569  subfacp1lem5  35574  inffz  36120  poimirlem2  38160  poimirlem6  38164  poimirlem7  38165  poimirlem8  38166  poimirlem11  38169  poimirlem15  38173  poimirlem16  38174  poimirlem17  38175  poimirlem19  38177  poimirlem20  38178  poimirlem22  38180  poimirlem24  38182  poimirlem29  38187  poimirlem31  38189  poimirlem32  38190  mblfinlem2  38196  fdc  38283  aks6d1c1  42772  aks6d1c5lem1  42792  sticksstones6  42807  sticksstones7  42808  sticksstones10  42811  sticksstones12a  42813  sticksstones12  42814  bcled  42834  bcle2d  42835  unitscyglem2  42852  unitscyglem4  42854  irrapxlem3  43442  acongrep  43598  fzmaxdif  43599  acongeq  43601  jm2.23  43614  jm2.26lem3  43619  jm2.27dlem2  43628  monoords  45907  fmul01lt1lem1  46191  fmul01lt1lem2  46192  sumnnodd  46237  limsupubuzlem  46317  dvnmul  46548  dvnprodlem1  46551  dvnprodlem2  46552  iblspltprt  46578  itgspltprt  46584  stoweidlem3  46608  stoweidlem11  46616  stoweidlem20  46625  stoweidlem26  46631  stoweidlem34  46639  wallispi2  46678  dirkeritg  46707  fourierdlem11  46723  fourierdlem12  46724  fourierdlem15  46727  fourierdlem41  46753  fourierdlem48  46759  fourierdlem49  46760  fourierdlem50  46761  fourierdlem52  46763  fourierdlem54  46765  fourierdlem79  46790  fourierdlem102  46813  fourierdlem103  46814  fourierdlem104  46815  fourierdlem114  46825  elaa2lem  46838  etransclem3  46842  etransclem4  46843  etransclem7  46846  etransclem10  46849  etransclem23  46862  etransclem24  46863  etransclem31  46870  etransclem32  46871  etransclem35  46874  etransclem41  46880  etransclem46  46885  caratheodorylem1  47131  iccpartgt  48064