Metamath Proof Explorer

Theorem elfzouz2

Description: The upper bound of a half-open range is greater than or equal to an element of the range. (Contributed by Mario Carneiro, 29-Sep-2015)

		Ref	Expression
	Assertion	elfzouz2	$⊢ K \in (M ..^N) \to N \in ℤ_{\geq K}$

Proof

Step	Hyp	Ref	Expression
1		elfzoelz	$⊢ K \in (M ..^N) \to K \in ℤ$
2		elfzoel2	$⊢ K \in (M ..^N) \to N \in ℤ$
3		elfzolt2	$⊢ K \in (M ..^N) \to K < N$
4		zre	$⊢ K \in ℤ \to K \in ℝ$
5		zre	$⊢ N \in ℤ \to N \in ℝ$
6		ltle	$⊢ (K \in ℝ \land N \in ℝ) \to (K < N \to K \leq N)$
7	4 5 6	syl2an	$⊢ (K \in ℤ \land N \in ℤ) \to (K < N \to K \leq N)$
8	1 2 7	syl2anc	$⊢ K \in (M ..^N) \to (K < N \to K \leq N)$
9	3 8	mpd	$⊢ K \in (M ..^N) \to K \leq N$
10		eluz2	$⊢ N \in ℤ_{\geq K} \leftrightarrow (K \in ℤ \land N \in ℤ \land K \leq N)$
11	1 2 9 10	syl3anbrc	$⊢ K \in (M ..^N) \to N \in ℤ_{\geq K}$