Theorem elfzle1 13454

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5110  ‘cfv 6501  (class class class)co 7362   ≤ cle 11199  ℤ_≥cuz 12772  ...cfz 13434

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677  ax-cnex 11116  ax-resscn 11117

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-1st 7926  df-2nd 7927  df-neg 11397  df-z 12509  df-uz 12773  df-fz 13435

This theorem is referenced by:  elfz1eq  13462  fzdisj  13478  elfznn  13480  ssfzunsnext  13496  fznatpl1  13505  fznn0sub2  13558  fz0fzdiffz0  13560  difelfznle  13565  seqf1olem1  13957  seqf1olem2  13958  bcval4  14217  seqcoll  14375  seqcoll2  14376  fsum0diaglem  15672  mertenslem1  15780  fprodntriv  15836  fallfacval4  15937  divalglem6  16291  hashdvds  16658  prmdiveq  16669  4sqlem11  16838  4sqlem12  16839  dvfsumlem3  25429  birthdaylem3  26340  ppiltx  26563  ppiub  26589  lgsdilem2  26718  lgsquadlem1  26765  chtppilimlem1  26858  dchrvmasumiflem1  26886  pntrlog2bndlem5  26966  pntpbnd1  26971  pntpbnd2  26972  pntlemh  26984  pntlemj  26988  ostth2lem2  27019  axlowdimlem16  27969  fzto1st1  32021  smattr  32469  smatbl  32470  smatbr  32471  ballotlem2  33177  ballotlemsdom  33200  ballotlemsima  33204  ballotlemfrcn0  33218  ballotlem1ri  33223  breprexplemc  33334  subfacp1lem1  33860  subfacp1lem5  33865  inffz  34388  poimirlem2  36153  poimirlem6  36157  poimirlem7  36158  poimirlem8  36159  poimirlem11  36162  poimirlem15  36166  poimirlem16  36167  poimirlem17  36168  poimirlem19  36170  poimirlem20  36171  poimirlem22  36173  poimirlem24  36175  poimirlem29  36180  poimirlem31  36182  poimirlem32  36183  mblfinlem2  36189  fdc  36277  sticksstones6  40632  sticksstones7  40633  sticksstones10  40636  sticksstones12a  40638  sticksstones12  40639  metakunt15  40664  irrapxlem3  41205  acongrep  41362  fzmaxdif  41363  acongeq  41365  jm2.23  41378  jm2.26lem3  41383  jm2.27dlem2  41392  monoords  43652  fmul01lt1lem1  43945  fmul01lt1lem2  43946  sumnnodd  43991  limsupubuzlem  44073  dvnmul  44304  dvnprodlem1  44307  dvnprodlem2  44308  iblspltprt  44334  itgspltprt  44340  stoweidlem3  44364  stoweidlem11  44372  stoweidlem20  44381  stoweidlem26  44387  stoweidlem34  44395  wallispi2  44434  dirkeritg  44463  fourierdlem11  44479  fourierdlem12  44480  fourierdlem15  44483  fourierdlem41  44509  fourierdlem48  44515  fourierdlem49  44516  fourierdlem50  44517  fourierdlem52  44519  fourierdlem54  44521  fourierdlem79  44546  fourierdlem102  44569  fourierdlem103  44570  fourierdlem104  44571  fourierdlem114  44581  elaa2lem  44594  etransclem3  44598  etransclem4  44599  etransclem7  44602  etransclem10  44605  etransclem23  44618  etransclem24  44619  etransclem31  44626  etransclem32  44627  etransclem35  44630  etransclem41  44636  etransclem46  44641  caratheodorylem1  44887  iccpartgt  45739