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 \in (M ..^N) \to M < N$

Step	Hyp	Ref	Expression
1		elfzoel1	$⊢ K \in (M ..^N) \to M \in ℤ$
2	1	zred	$⊢ K \in (M ..^N) \to M \in ℝ$
3		elfzoelz	$⊢ K \in (M ..^N) \to K \in ℤ$
4	3	zred	$⊢ K \in (M ..^N) \to K \in ℝ$
5		elfzoel2	$⊢ K \in (M ..^N) \to N \in ℤ$
6	5	zred	$⊢ K \in (M ..^N) \to N \in ℝ$
7		elfzole1	$⊢ K \in (M ..^N) \to M \leq K$
8		elfzolt2	$⊢ K \in (M ..^N) \to K < N$
9	2 4 6 7 8	lelttrd	$⊢ K \in (M ..^N) \to M < N$

Metamath Proof Explorer