Theorem elfzle1 13555

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 13548	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		eluzle 12875	. 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 11244  ℤ_≥cuz 12862  ...cfz 13535

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 11156  ax-resscn 11157

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 7986  df-2nd 7987  df-neg 11444  df-z 12592  df-uz 12863  df-fz 13536

This theorem is referenced by:  elfz1eq  13563  fzdisj  13579  elfznn  13581  ssfzunsnext  13597  fznatpl1  13606  fznn0sub2  13663  fz0fzdiffz0  13665  difelfznle  13670  seqf1olem1  14077  seqf1olem2  14078  bcval4  14343  seqcoll  14501  seqcoll2  14502  fsum0diaglem  15827  mertenslem1  15938  fprodntriv  15996  fallfacval4  16097  divalglem6  16456  hashdvds  16834  prmdiveq  16845  4sqlem11  17015  4sqlem12  17016  dvfsumlem3  26156  birthdaylem3  27084  ppiltx  27307  ppiub  27334  lgsdilem2  27463  lgsquadlem1  27510  chtppilimlem1  27603  dchrvmasumiflem1  27631  pntrlog2bndlem5  27711  pntpbnd1  27716  pntpbnd2  27717  pntlemh  27729  pntlemj  27733  ostth2lem2  27764  axlowdimlem16  29248  fzto1st1  33363  smattr  34134  smatbl  34135  smatbr  34136  ballotlem2  34824  ballotlemsdom  34847  ballotlemsima  34851  ballotlemfrcn0  34865  ballotlem1ri  34870  breprexplemc  34964  subfacp1lem1  35570  subfacp1lem5  35575  inffz  36121  poimirlem2  38161  poimirlem6  38165  poimirlem7  38166  poimirlem8  38167  poimirlem11  38170  poimirlem15  38174  poimirlem16  38175  poimirlem17  38176  poimirlem19  38178  poimirlem20  38179  poimirlem22  38181  poimirlem24  38183  poimirlem29  38188  poimirlem31  38190  poimirlem32  38191  mblfinlem2  38197  fdc  38284  aks6d1c1  42773  aks6d1c5lem1  42793  sticksstones6  42808  sticksstones7  42809  sticksstones10  42812  sticksstones12a  42814  sticksstones12  42815  bcled  42835  bcle2d  42836  unitscyglem2  42853  unitscyglem4  42855  irrapxlem3  43443  acongrep  43599  fzmaxdif  43600  acongeq  43602  jm2.23  43615  jm2.26lem3  43620  jm2.27dlem2  43629  monoords  45908  fmul01lt1lem1  46192  fmul01lt1lem2  46193  sumnnodd  46238  limsupubuzlem  46318  dvnmul  46549  dvnprodlem1  46552  dvnprodlem2  46553  iblspltprt  46579  itgspltprt  46585  stoweidlem3  46609  stoweidlem11  46617  stoweidlem20  46626  stoweidlem26  46632  stoweidlem34  46640  wallispi2  46679  dirkeritg  46708  fourierdlem11  46724  fourierdlem12  46725  fourierdlem15  46728  fourierdlem41  46754  fourierdlem48  46760  fourierdlem49  46761  fourierdlem50  46762  fourierdlem52  46764  fourierdlem54  46766  fourierdlem79  46791  fourierdlem102  46814  fourierdlem103  46815  fourierdlem104  46816  fourierdlem114  46826  elaa2lem  46839  etransclem3  46843  etransclem4  46844  etransclem7  46847  etransclem10  46850  etransclem23  46863  etransclem24  46864  etransclem31  46871  etransclem32  46872  etransclem35  46875  etransclem41  46881  etransclem46  46886  caratheodorylem1  47132  iccpartgt  48065