Theorem nn0absid

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

	Ref	Expression
Assertion	nn0absid	⊢ ( 𝑁 ∈ ℕ0 → ( abs ‘ 𝑁 ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
2		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
3	1 2	absidd	⊢ ( 𝑁 ∈ ℕ0 → ( abs ‘ 𝑁 ) = 𝑁 )