Metamath Proof Explorer


Theorem elfzle2

Description: A member of a finite set of sequential integer is less than or equal to the upper bound. (Contributed by NM, 6-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion elfzle2
|- ( K e. ( M ... N ) -> K <_ N )

Proof

Step Hyp Ref Expression
1 elfzuz3
 |-  ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) )
2 eluzle
 |-  ( N e. ( ZZ>= ` K ) -> K <_ N )
3 1 2 syl
 |-  ( K e. ( M ... N ) -> K <_ N )