Metamath Proof Explorer

Theorem elfzolem1

Description: A member in a half-open integer interval is less than or equal to the upper bound minus 1 . (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Assertion	elfzolem1	$⊢ K \in (M ..^N) \to K \leq N - 1$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ K \in (M ..^N) \to K \in (M ..^N)$
2		elfzoel2	$⊢ K \in (M ..^N) \to N \in ℤ$
3		simpl	$⊢ (K \in (M ..^N) \land N \in ℤ) \to K \in (M ..^N)$
4		fzoval	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$
5	4	adantl	$⊢ (K \in (M ..^N) \land N \in ℤ) \to (M ..^N) = (M \dots N - 1)$
6	3 5	eleqtrd	$⊢ (K \in (M ..^N) \land N \in ℤ) \to K \in (M \dots N - 1)$
7		elfzle2	$⊢ K \in (M \dots N - 1) \to K \leq N - 1$
8	6 7	syl	$⊢ (K \in (M ..^N) \land N \in ℤ) \to K \leq N - 1$
9	1 2 8	syl2anc	$⊢ K \in (M ..^N) \to K \leq N - 1$