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

Metamath Proof Explorer

Theorem nn0absidi

Description: A nonnegative integer is its own absolute value (inference form). (Contributed by AV, 22-Nov-2025)

		Ref	Expression
	Hypothesis	nn0absidi.i	$⊢ N \in ℕ_{0}$
	Assertion	nn0absidi	$⊢ \|N\| = N$

Step	Hyp	Ref	Expression
1		nn0absidi.i	$⊢ N \in ℕ_{0}$
2		nn0absid	$⊢ N \in ℕ_{0} \to \|N\| = N$
3	1 2	ax-mp	$⊢ \|N\| = N$