Metamath Proof Explorer

Theorem elfzop1le2

Description: A member in a half-open integer interval plus 1 is less than or equal to the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		elfzolt2	$⊢ K \in (M ..^N) \to K < N$
2		elfzoelz	$⊢ K \in (M ..^N) \to K \in ℤ$
3		elfzoel2	$⊢ K \in (M ..^N) \to N \in ℤ$
4		zltp1le	$⊢ (K \in ℤ \land N \in ℤ) \to (K < N \leftrightarrow K + 1 \leq N)$
5	2 3 4	syl2anc	$⊢ K \in (M ..^N) \to (K < N \leftrightarrow K + 1 \leq N)$
6	1 5	mpbid	$⊢ K \in (M ..^N) \to K + 1 \leq N$