Theorem elfzole1

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

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

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	simpld	|- ( K e. ( M ..^ N ) -> M <_ K )