Metamath Proof Explorer

Theorem gcdn0cl

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

Ref Expression
Assertion gcdn0cl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N ∈ ℕ

Proof

Step Hyp Ref Expression
1 gcdn0val ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N = sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <
2 eqid ⊢ n ∈ ℤ | ∀ z ∈ M N n ∥ z = n ∈ ℤ | ∀ z ∈ M N n ∥ z
3 eqid ⊢ n ∈ ℤ | n ∥ M ∧ n ∥ N = n ∈ ℤ | n ∥ M ∧ n ∥ N
4 2 3 gcdcllem3 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∈ ℕ ∧ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∥ M ∧ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∥ N ∧ K ∈ ℤ ∧ K ∥ M ∧ K ∥ N → K ≤ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <
5 4 simp1d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∈ ℕ
6 1 5 eqeltrd ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N ∈ ℕ