Metamath Proof Explorer

Theorem elfzr

Description: A member of a finite interval of integers is either a member of the corresponding half-open integer range or the upper bound of the interval. (Contributed by AV, 5-Feb-2021)

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

Proof

Step	Hyp	Ref	Expression
1		elfzuz2	$⊢ K \in (M \dots N) \to N \in ℤ_{\geq M}$
2		fzisfzounsn	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = (M ..^N) \cup \{N\}$
3	2	eleq2d	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N) \leftrightarrow K \in ((M ..^N) \cup \{N\}))$
4		elun	$⊢ K \in ((M ..^N) \cup \{N\}) \leftrightarrow (K \in (M ..^N) \lor K \in \{N\})$
5		elsni	$⊢ K \in \{N\} \to K = N$
6	5	orim2i	$⊢ (K \in (M ..^N) \lor K \in \{N\}) \to (K \in (M ..^N) \lor K = N)$
7	4 6	sylbi	$⊢ K \in ((M ..^N) \cup \{N\}) \to (K \in (M ..^N) \lor K = N)$
8	3 7	biimtrdi	$⊢ N \in ℤ_{\geq M} \to (K \in (M \dots N) \to (K \in (M ..^N) \lor K = N))$
9	1 8	mpcom	$⊢ K \in (M \dots N) \to (K \in (M ..^N) \lor K = N)$