Metamath Proof Explorer


Theorem elfzolt2

Description: A member in a half-open integer interval is less than the upper bound. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion elfzolt2
|- ( K e. ( M ..^ N ) -> K < N )

Proof

Step Hyp Ref Expression
1 elfzoelz
 |-  ( K e. ( M ..^ N ) -> K e. ZZ )
2 elfzoel1
 |-  ( K e. ( M ..^ N ) -> M e. ZZ )
3 elfzoel2
 |-  ( K e. ( M ..^ N ) -> N e. ZZ )
4 elfzo
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K e. ( M ..^ N ) <-> ( M <_ K /\ K < N ) ) )
5 1 2 3 4 syl3anc
 |-  ( K e. ( M ..^ N ) -> ( K e. ( M ..^ N ) <-> ( M <_ K /\ K < N ) ) )
6 5 ibi
 |-  ( K e. ( M ..^ N ) -> ( M <_ K /\ K < N ) )
7 6 simprd
 |-  ( K e. ( M ..^ N ) -> K < N )