Metamath Proof Explorer

Theorem gcdnncl

Description: Closure of the gcd operator. (Contributed by Thierry Arnoux, 2-Feb-2020)

Ref Expression
Assertion gcdnncl ⊢ M ∈ ℕ ∧ N ∈ ℕ → M gcd N ∈ ℕ

Proof

Step Hyp Ref Expression
1 simpl ⊢ M ∈ ℕ ∧ N ∈ ℕ → M ∈ ℕ
2 1 nnzd ⊢ M ∈ ℕ ∧ N ∈ ℕ → M ∈ ℤ
3 simpr ⊢ M ∈ ℕ ∧ N ∈ ℕ → N ∈ ℕ
4 3 nnzd ⊢ M ∈ ℕ ∧ N ∈ ℕ → N ∈ ℤ
5 3 nnne0d ⊢ M ∈ ℕ ∧ N ∈ ℕ → N ≠ 0
6 5 neneqd ⊢ M ∈ ℕ ∧ N ∈ ℕ → ¬ N = 0
7 6 intnand ⊢ M ∈ ℕ ∧ N ∈ ℕ → ¬ M = 0 ∧ N = 0
8 gcdn0cl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N ∈ ℕ
9 2 4 7 8 syl21anc ⊢ M ∈ ℕ ∧ N ∈ ℕ → M gcd N ∈ ℕ