Metamath Proof Explorer

Theorem elfzlmr

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

		Ref	Expression
	Assertion	elfzlmr	$⊢ K \in (M \dots N) \to (K = M \lor K \in (M + 1 ..^N) \lor K = N)$

Proof

Step	Hyp	Ref	Expression
1		elfzuz2	$⊢ K \in (M \dots N) \to N \in ℤ_{\geq M}$
2		fzpred	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = \{M\} \cup (M + 1 \dots N)$
3	2	eleq2d	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N) \leftrightarrow K \in (\{M\} \cup (M + 1 \dots N)))$
4		elsni	$⊢ K \in \{M\} \to K = M$
5		elfzr	$⊢ K \in (M + 1 \dots N) \to (K \in (M + 1 ..^N) \lor K = N)$
6	4 5	orim12i	$⊢ (K \in \{M\} \lor K \in (M + 1 \dots N)) \to (K = M \lor (K \in (M + 1 ..^N) \lor K = N))$
7		elun	$⊢ K \in (\{M\} \cup (M + 1 \dots N)) \leftrightarrow (K \in \{M\} \lor K \in (M + 1 \dots N))$
8		3orass	$⊢ (K = M \lor K \in (M + 1 ..^N) \lor K = N) \leftrightarrow (K = M \lor (K \in (M + 1 ..^N) \lor K = N))$
9	6 7 8	3imtr4i	$⊢ K \in (\{M\} \cup (M + 1 \dots N)) \to (K = M \lor K \in (M + 1 ..^N) \lor K = N)$
10	3 9	syl6bi	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N) \to (K = M \lor K \in (M + 1 ..^N) \lor K = N))$
11	1 10	mpcom	$⊢ K \in (M \dots N) \to (K = M \lor K \in (M + 1 ..^N) \lor K = N)$