Theorem nn0gcdid0

Description: The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011)

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

Proof

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