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