Theorem gcdnn0id

Description: The gcd of a nonnegative integer and itself is the integer. (Contributed by SN, 25-Aug-2024)

	Ref	Expression
Assertion	gcdnn0id	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 gcd 𝑁 ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
2		gcdid	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 gcd 𝑁 ) = ( abs ‘ 𝑁 ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 gcd 𝑁 ) = ( abs ‘ 𝑁 ) )
4		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
5		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
6	4 5	absidd	⊢ ( 𝑁 ∈ ℕ0 → ( abs ‘ 𝑁 ) = 𝑁 )
7	3 6	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 gcd 𝑁 ) = 𝑁 )