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

Metamath Proof Explorer

Theorem prednn0

Description: The value of the predecessor class over NN0 . (Contributed by Scott Fenton, 9-May-2014)

		Ref	Expression
	Assertion	prednn0	$⊢ N \in ℕ_{0} \to Pred (< ℕ_{0} N) = (0 \dots N - 1)$

Step	Hyp	Ref	Expression
1		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
2		predeq2	$⊢ ℕ_{0} = ℤ_{\geq 0} \to Pred (< ℕ_{0} N) = Pred (< ℤ_{\geq 0} N)$
3	1 2	ax-mp	$⊢ Pred (< ℕ_{0} N) = Pred (< ℤ_{\geq 0} N)$
4		preduz	$⊢ N \in ℤ_{\geq 0} \to Pred (< ℤ_{\geq 0} N) = (0 \dots N - 1)$
5	3 4	eqtrid	$⊢ N \in ℤ_{\geq 0} \to Pred (< ℕ_{0} N) = (0 \dots N - 1)$
6	5 1	eleq2s	$⊢ N \in ℕ_{0} \to Pred (< ℕ_{0} N) = (0 \dots N - 1)$