Theorem elfzle1 13568

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5142  ‘cfv 6560  (class class class)co 7432   ≤ cle 11297  ℤ_≥cuz 12879  ...cfz 13548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-1st 8015  df-2nd 8016  df-neg 11496  df-z 12616  df-uz 12880  df-fz 13549

This theorem is referenced by:  elfz1eq  13576  fzdisj  13592  elfznn  13594  ssfzunsnext  13610  fznatpl1  13619  fznn0sub2  13676  fz0fzdiffz0  13678  difelfznle  13683  seqf1olem1  14083  seqf1olem2  14084  bcval4  14347  seqcoll  14504  seqcoll2  14505  fsum0diaglem  15813  mertenslem1  15921  fprodntriv  15979  fallfacval4  16080  divalglem6  16436  hashdvds  16813  prmdiveq  16824  4sqlem11  16994  4sqlem12  16995  dvfsumlem3  26070  birthdaylem3  26997  ppiltx  27221  ppiub  27249  lgsdilem2  27378  lgsquadlem1  27425  chtppilimlem1  27518  dchrvmasumiflem1  27546  pntrlog2bndlem5  27626  pntpbnd1  27631  pntpbnd2  27632  pntlemh  27644  pntlemj  27648  ostth2lem2  27679  axlowdimlem16  28973  fzto1st1  33123  smattr  33799  smatbl  33800  smatbr  33801  ballotlem2  34492  ballotlemsdom  34515  ballotlemsima  34519  ballotlemfrcn0  34533  ballotlem1ri  34538  breprexplemc  34648  subfacp1lem1  35185  subfacp1lem5  35190  inffz  35731  poimirlem2  37630  poimirlem6  37634  poimirlem7  37635  poimirlem8  37636  poimirlem11  37639  poimirlem15  37643  poimirlem16  37644  poimirlem17  37645  poimirlem19  37647  poimirlem20  37648  poimirlem22  37650  poimirlem24  37652  poimirlem29  37657  poimirlem31  37659  poimirlem32  37660  mblfinlem2  37666  fdc  37753  aks6d1c1  42118  aks6d1c5lem1  42138  sticksstones6  42153  sticksstones7  42154  sticksstones10  42157  sticksstones12a  42159  sticksstones12  42160  bcled  42180  bcle2d  42181  unitscyglem2  42198  unitscyglem4  42200  metakunt15  42221  irrapxlem3  42840  acongrep  42997  fzmaxdif  42998  acongeq  43000  jm2.23  43013  jm2.26lem3  43018  jm2.27dlem2  43027  monoords  45314  fmul01lt1lem1  45604  fmul01lt1lem2  45605  sumnnodd  45650  limsupubuzlem  45732  dvnmul  45963  dvnprodlem1  45966  dvnprodlem2  45967  iblspltprt  45993  itgspltprt  45999  stoweidlem3  46023  stoweidlem11  46031  stoweidlem20  46040  stoweidlem26  46046  stoweidlem34  46054  wallispi2  46093  dirkeritg  46122  fourierdlem11  46138  fourierdlem12  46139  fourierdlem15  46142  fourierdlem41  46168  fourierdlem48  46174  fourierdlem49  46175  fourierdlem50  46176  fourierdlem52  46178  fourierdlem54  46180  fourierdlem79  46205  fourierdlem102  46228  fourierdlem103  46229  fourierdlem104  46230  fourierdlem114  46240  elaa2lem  46253  etransclem3  46257  etransclem4  46258  etransclem7  46261  etransclem10  46264  etransclem23  46277  etransclem24  46278  etransclem31  46285  etransclem32  46286  etransclem35  46289  etransclem41  46295  etransclem46  46300  caratheodorylem1  46546  iccpartgt  47419