Metamath Proof Explorer

Theorem gcdcl

Description: Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion gcdcl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 oveq12 ⊢ M = 0 ∧ N = 0 → M gcd N = 0 gcd 0
2 gcd0val ⊢ 0 gcd 0 = 0
3 1 2 eqtrdi ⊢ M = 0 ∧ N = 0 → M gcd N = 0
4 0nn0 ⊢ 0 ∈ ℕ 0
5 3 4 eqeltrdi ⊢ M = 0 ∧ N = 0 → M gcd N ∈ ℕ 0
6 5 adantl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 ∧ N = 0 → M gcd N ∈ ℕ 0
7 gcdn0cl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N ∈ ℕ
8 7 nnnn0d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N ∈ ℕ 0
9 6 8 pm2.61dan ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N ∈ ℕ 0