Metamath Proof Explorer

Theorem gcdn0val

Description: The value of the gcd operator when at least one operand is nonzero. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion gcdn0val ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N = sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <

Proof

Step Hyp Ref Expression
1 gcdval ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = if M = 0 ∧ N = 0 0 sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <
2 iffalse ⊢ ¬ M = 0 ∧ N = 0 → if M = 0 ∧ N = 0 0 sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < = sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <
3 1 2 sylan9eq ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N = sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <