Metamath Proof Explorer

Theorem fz0sn0fz1

Description: A finite set of sequential nonnegative integers is the union of the singleton containing 0 and a finite set of sequential positive integers. (Contributed by AV, 20-Mar-2021)

		Ref	Expression
	Assertion	fz0sn0fz1	$⊢ N \in ℕ_{0} \to (0 \dots N) = \{0\} \cup (1 \dots N)$

Proof

Step	Hyp	Ref	Expression
1		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
2		fzsplit	$⊢ 0 \in (0 \dots N) \to (0 \dots N) = (0 \dots 0) \cup (0 + 1 \dots N)$
3		0p1e1	$⊢ 0 + 1 = 1$
4	3	oveq1i	$⊢ (0 + 1 \dots N) = (1 \dots N)$
5	4	uneq2i	$⊢ (0 \dots 0) \cup (0 + 1 \dots N) = (0 \dots 0) \cup (1 \dots N)$
6	2 5	eqtrdi	$⊢ 0 \in (0 \dots N) \to (0 \dots N) = (0 \dots 0) \cup (1 \dots N)$
7	1 6	syl	$⊢ N \in ℕ_{0} \to (0 \dots N) = (0 \dots 0) \cup (1 \dots N)$
8		0z	$⊢ 0 \in ℤ$
9		fzsn	$⊢ 0 \in ℤ \to (0 \dots 0) = \{0\}$
10	8 9	mp1i	$⊢ N \in ℕ_{0} \to (0 \dots 0) = \{0\}$
11	10	uneq1d	$⊢ N \in ℕ_{0} \to (0 \dots 0) \cup (1 \dots N) = \{0\} \cup (1 \dots N)$
12	7 11	eqtrd	$⊢ N \in ℕ_{0} \to (0 \dots N) = \{0\} \cup (1 \dots N)$