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