fzpred

Description: Join a predecessor to the beginning of a finite set of sequential integers. (Contributed by AV, 24-Aug-2019)

		Ref	Expression
	Assertion	fzpred	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = \{M\} \cup (M + 1 \dots N)$

Step	Hyp	Ref	Expression
1		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
2		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
3		peano2uz	$⊢ M \in ℤ_{\geq M} \to M + 1 \in ℤ_{\geq M}$
4	1 2 3	3syl	$⊢ N \in ℤ_{\geq M} \to M + 1 \in ℤ_{\geq M}$
5		fzsplit2	$⊢ (M + 1 \in ℤ_{\geq M} \land N \in ℤ_{\geq M}) \to (M \dots N) = (M \dots M) \cup (M + 1 \dots N)$
6	4 5	mpancom	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = (M \dots M) \cup (M + 1 \dots N)$
7		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
8	1 7	syl	$⊢ N \in ℤ_{\geq M} \to (M \dots M) = \{M\}$
9	8	uneq1d	$⊢ N \in ℤ_{\geq M} \to (M \dots M) \cup (M + 1 \dots N) = \{M\} \cup (M + 1 \dots N)$
10	6 9	eqtrd	$⊢ N \in ℤ_{\geq M} \to (M \dots N) = \{M\} \cup (M + 1 \dots N)$

Metamath Proof Explorer