Metamath Proof Explorer

Theorem gcdeq0

Description: The gcd of two integers is zero iff they are both zero. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion gcdeq0 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = 0 ↔ M = 0 ∧ N = 0

Proof

Step Hyp Ref Expression
1 gcdn0cl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N ∈ ℕ
2 1 nnne0d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N ≠ 0
3 2 ex ⊢ M ∈ ℤ ∧ N ∈ ℤ → ¬ M = 0 ∧ N = 0 → M gcd N ≠ 0
4 3 necon4bd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = 0 → M = 0 ∧ N = 0
5 oveq12 ⊢ M = 0 ∧ N = 0 → M gcd N = 0 gcd 0
6 gcd0val ⊢ 0 gcd 0 = 0
7 5 6 eqtrdi ⊢ M = 0 ∧ N = 0 → M gcd N = 0
8 4 7 impbid1 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = 0 ↔ M = 0 ∧ N = 0