Theorem elfzolt3

Description: Membership in a half-open integer interval implies that the bounds are unequal. (Contributed by Stefan O'Rear, 15-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		elfzoel1	|- ( K e. ( M ..^ N ) -> M e. ZZ )
2	1	zred	|- ( K e. ( M ..^ N ) -> M e. RR )
3		elfzoelz	|- ( K e. ( M ..^ N ) -> K e. ZZ )
4	3	zred	|- ( K e. ( M ..^ N ) -> K e. RR )
5		elfzoel2	|- ( K e. ( M ..^ N ) -> N e. ZZ )
6	5	zred	|- ( K e. ( M ..^ N ) -> N e. RR )
7		elfzole1	|- ( K e. ( M ..^ N ) -> M <_ K )
8		elfzolt2	|- ( K e. ( M ..^ N ) -> K < N )
9	2 4 6 7 8	lelttrd	|- ( K e. ( M ..^ N ) -> M < N )