Metamath Proof Explorer

Theorem gcd2n0cl

Description: Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 neneq ⊢ N ≠ 0 → ¬ N = 0
2 1 intnand ⊢ N ≠ 0 → ¬ M = 0 ∧ N = 0
3 2 anim2i ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0
4 3 3impa ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0
5 gcdn0cl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N ∈ ℕ
6 4 5 syl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 → M gcd N ∈ ℕ