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

Step	Hyp	Ref	Expression
1		elfzoelz	$⊢ K \in (M ..^N) \to K \in ℤ$
2		elfzoel1	$⊢ K \in (M ..^N) \to M \in ℤ$
3		elfzoel2	$⊢ K \in (M ..^N) \to N \in ℤ$
4		elfzo	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in (M ..^N) \leftrightarrow (M \leq K \land K < N))$
5	1 2 3 4	syl3anc	$⊢ K \in (M ..^N) \to (K \in (M ..^N) \leftrightarrow (M \leq K \land K < N))$
6	5	ibi	$⊢ K \in (M ..^N) \to (M \leq K \land K < N)$
7	6	simpld	$⊢ K \in (M ..^N) \to M \leq K$

Metamath Proof Explorer