Metamath Proof Explorer

Theorem elfz0lmr

Description: A member of a finite interval of nonnegative integers is either 0 or its upper bound or an element of its interior. (Contributed by AV, 5-Feb-2021)

		Ref	Expression
	Assertion	elfz0lmr	$⊢ K \in (0 \dots N) \to (K = 0 \lor K \in (1 ..^N) \lor K = N)$

Proof

Step	Hyp	Ref	Expression
1		elfzlmr	$⊢ K \in (0 \dots N) \to (K = 0 \lor K \in (0 + 1 ..^N) \lor K = N)$
2		biid	$⊢ K = 0 \leftrightarrow K = 0$
3		0p1e1	$⊢ 0 + 1 = 1$
4	3	oveq1i	$⊢ (0 + 1 ..^N) = (1 ..^N)$
5	4	eleq2i	$⊢ K \in (0 + 1 ..^N) \leftrightarrow K \in (1 ..^N)$
6		biid	$⊢ K = N \leftrightarrow K = N$
7	2 5 6	3orbi123i	$⊢ (K = 0 \lor K \in (0 + 1 ..^N) \lor K = N) \leftrightarrow (K = 0 \lor K \in (1 ..^N) \lor K = N)$
8	1 7	sylib	$⊢ K \in (0 \dots N) \to (K = 0 \lor K \in (1 ..^N) \lor K = N)$