Metamath Proof Explorer

Theorem elfzolt2b

Description: A member in a half-open integer interval is less than the upper bound. (Contributed by Mario Carneiro, 29-Sep-2015)

		Ref	Expression
	Assertion	elfzolt2b	$⊢ K \in (M ..^N) \to K \in (K ..^N)$

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		fzolb	$⊢ K \in (K ..^N) \leftrightarrow (K \in ℤ \land N \in ℤ \land K < N)$
5	1 2 3 4	syl3anbrc	$⊢ K \in (M ..^N) \to K \in (K ..^N)$