Theorem nn0absidi

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

	Ref	Expression
Hypothesis	nn0absidi.i	⊢ 𝑁 ∈ ℕ0
Assertion	nn0absidi	⊢ ( abs ‘ 𝑁 ) = 𝑁

Proof

Step	Hyp	Ref	Expression
1		nn0absidi.i	⊢ 𝑁 ∈ ℕ0
2		nn0absid	⊢ ( 𝑁 ∈ ℕ0 → ( abs ‘ 𝑁 ) = 𝑁 )
3	1 2	ax-mp	⊢ ( abs ‘ 𝑁 ) = 𝑁