Metamath Proof Explorer


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 ) = 𝑁 )