fzne1

Description: Elementhood in a finite set of sequential integers, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024)

		Ref	Expression
	Assertion	fzne1	$⊢ (K \in (M \dots N) \land K \neq M) \to K \in (M + 1 \dots N)$

Step	Hyp	Ref	Expression
1		df-ne	$⊢ K \neq M \leftrightarrow \neg K = M$
2		elfzuz2	$⊢ K \in (M \dots N) \to N \in ℤ_{\geq M}$
3		elfzp12	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N) \leftrightarrow (K = M \lor K \in (M + 1 \dots N)))$
4	2 3	syl	$⊢ K \in (M \dots N) \to (K \in (M \dots N) \leftrightarrow (K = M \lor K \in (M + 1 \dots N)))$
5	4	ibi	$⊢ K \in (M \dots N) \to (K = M \lor K \in (M + 1 \dots N))$
6	5	orcanai	$⊢ (K \in (M \dots N) \land \neg K = M) \to K \in (M + 1 \dots N)$
7	1 6	sylan2b	$⊢ (K \in (M \dots N) \land K \neq M) \to K \in (M + 1 \dots N)$

Metamath Proof Explorer