This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fz0dif1

Description: Split the first element of a finite set of sequential nonnegative integers. (Contributed by AV, 12-Sep-2025)

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

Step	Hyp	Ref	Expression
1		elnn0uz	$⊢ N \in ℕ_{0} \leftrightarrow N \in ℤ_{\geq 0}$
2		fzdif1	$⊢ N \in ℤ_{\geq 0} \to (0 \dots N) ∖ \{0\} = (0 + 1 \dots N)$
3	1 2	sylbi	$⊢ N \in ℕ_{0} \to (0 \dots N) ∖ \{0\} = (0 + 1 \dots N)$
4		0p1e1	$⊢ 0 + 1 = 1$
5	4	oveq1i	$⊢ (0 + 1 \dots N) = (1 \dots N)$
6	3 5	eqtrdi	$⊢ N \in ℕ_{0} \to (0 \dots N) ∖ \{0\} = (1 \dots N)$