Metamath Proof Explorer

Theorem fzsuc

Description: Join a successor to the end of a finite set of sequential integers. (Contributed by NM, 19-Jul-2008) (Revised by Mario Carneiro, 28-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		peano2uz	$⊢ N \in ℤ_{\geq M} \to N + 1 \in ℤ_{\geq M}$
2		eluzfz2	$⊢ N + 1 \in ℤ_{\geq M} \to N + 1 \in (M \dots N + 1)$
3	1 2	syl	$⊢ N \in ℤ_{\geq M} \to N + 1 \in (M \dots N + 1)$
4		peano2fzr	$⊢ (N \in ℤ_{\geq M} \land N + 1 \in (M \dots N + 1)) \to N \in (M \dots N + 1)$
5	3 4	mpdan	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N + 1)$
6		fzsplit	$⊢ N \in (M \dots N + 1) \to (M \dots N + 1) = (M \dots N) \cup (N + 1 \dots N + 1)$
7	5 6	syl	$⊢ N \in ℤ_{\geq M} \to (M \dots N + 1) = (M \dots N) \cup (N + 1 \dots N + 1)$
8		eluzelz	$⊢ N + 1 \in ℤ_{\geq M} \to N + 1 \in ℤ$
9		fzsn	$⊢ N + 1 \in ℤ \to (N + 1 \dots N + 1) = \{N + 1\}$
10	1 8 9	3syl	$⊢ N \in ℤ_{\geq M} \to (N + 1 \dots N + 1) = \{N + 1\}$
11	10	uneq2d	$⊢ N \in ℤ_{\geq M} \to (M \dots N) \cup (N + 1 \dots N + 1) = (M \dots N) \cup \{N + 1\}$
12	7 11	eqtrd	$⊢ N \in ℤ_{\geq M} \to (M \dots N + 1) = (M \dots N) \cup \{N + 1\}$