# 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 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\mathrm{gcd}{N}=0↔\left({M}=0\wedge {N}=0\right)\right)$

### Proof

Step Hyp Ref Expression
1 gcdn0cl ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to {M}\mathrm{gcd}{N}\in ℕ$
2 1 nnne0d ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge ¬\left({M}=0\wedge {N}=0\right)\right)\to {M}\mathrm{gcd}{N}\ne 0$
3 2 ex ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left(¬\left({M}=0\wedge {N}=0\right)\to {M}\mathrm{gcd}{N}\ne 0\right)$
4 3 necon4bd ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\mathrm{gcd}{N}=0\to \left({M}=0\wedge {N}=0\right)\right)$
5 oveq12 ${⊢}\left({M}=0\wedge {N}=0\right)\to {M}\mathrm{gcd}{N}=0\mathrm{gcd}0$
6 gcd0val ${⊢}0\mathrm{gcd}0=0$
7 5 6 syl6eq ${⊢}\left({M}=0\wedge {N}=0\right)\to {M}\mathrm{gcd}{N}=0$
8 4 7 impbid1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\mathrm{gcd}{N}=0↔\left({M}=0\wedge {N}=0\right)\right)$