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 e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) = 0 <-> ( M = 0 /\ N = 0 ) ) )

Proof

Step Hyp Ref Expression
1 gcdn0cl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) e. NN )
2 1 nnne0d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) =/= 0 )
3 2 ex 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -. ( M = 0 /\ N = 0 ) -> ( M gcd N ) =/= 0 ) )
4 3 necon4bd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( 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 e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) = 0 <-> ( M = 0 /\ N = 0 ) ) )