Theorem elfzle1 12911

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5066  ‘cfv 6355  (class class class)co 7156   ≤ cle 10676  ℤ_≥cuz 12244  ...cfz 12893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-1st 7689  df-2nd 7690  df-neg 10873  df-z 11983  df-uz 12245  df-fz 12894

This theorem is referenced by:  elfz1eq  12919  fzdisj  12935  elfznn  12937  ssfzunsnext  12953  fznatpl1  12962  fznn0sub2  13015  fz0fzdiffz0  13017  difelfznle  13022  seqf1olem1  13410  seqf1olem2  13411  bcval4  13668  seqcoll  13823  seqcoll2  13824  fsum0diaglem  15131  mertenslem1  15240  fprodntriv  15296  fallfacval4  15397  divalglem6  15749  hashdvds  16112  prmdiveq  16123  4sqlem11  16291  4sqlem12  16292  dvfsumlem3  24625  birthdaylem3  25531  ppiltx  25754  ppiub  25780  lgsdilem2  25909  lgsquadlem1  25956  chtppilimlem1  26049  dchrvmasumiflem1  26077  pntrlog2bndlem5  26157  pntpbnd1  26162  pntpbnd2  26163  pntlemh  26175  pntlemj  26179  ostth2lem2  26210  axlowdimlem16  26743  fzto1st1  30744  smattr  31064  smatbl  31065  smatbr  31066  ballotlem2  31746  ballotlemsdom  31769  ballotlemsima  31773  ballotlemfrcn0  31787  ballotlem1ri  31792  breprexplemc  31903  subfacp1lem1  32426  subfacp1lem5  32431  inffz  32961  poimirlem2  34909  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem11  34918  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem22  34929  poimirlem24  34931  poimirlem29  34936  poimirlem31  34938  poimirlem32  34939  mblfinlem2  34945  fdc  35035  irrapxlem3  39441  acongrep  39597  fzmaxdif  39598  acongeq  39600  jm2.23  39613  jm2.26lem3  39618  jm2.27dlem2  39627  monoords  41584  fmul01lt1lem1  41885  fmul01lt1lem2  41886  sumnnodd  41931  limsupubuzlem  42013  dvnmul  42248  dvnprodlem1  42251  dvnprodlem2  42252  iblspltprt  42278  itgspltprt  42284  stoweidlem3  42308  stoweidlem11  42316  stoweidlem20  42325  stoweidlem26  42331  stoweidlem34  42339  wallispi2  42378  dirkeritg  42407  fourierdlem11  42423  fourierdlem12  42424  fourierdlem15  42427  fourierdlem41  42453  fourierdlem48  42459  fourierdlem49  42460  fourierdlem50  42461  fourierdlem52  42463  fourierdlem54  42465  fourierdlem79  42490  fourierdlem102  42513  fourierdlem103  42514  fourierdlem104  42515  fourierdlem114  42525  elaa2lem  42538  etransclem3  42542  etransclem4  42543  etransclem7  42546  etransclem10  42549  etransclem23  42562  etransclem24  42563  etransclem31  42570  etransclem32  42571  etransclem35  42574  etransclem41  42580  etransclem46  42585  caratheodorylem1  42828  iccpartgt  43607