Metamath Proof Explorer

Theorem gcdn0gt0

Description: The gcd of two integers is positive (nonzero) iff they are not both zero. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion gcdn0gt0 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( -. ( M = 0 /\ N = 0 ) <-> 0 < ( M gcd N ) ) )

Proof

Step Hyp Ref Expression
1 gcdcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )
2 0re 
 |-  0 e. RR
3 nn0re 
 |-  ( ( M gcd N ) e. NN0 -> ( M gcd N ) e. RR )
4 nn0ge0 
 |-  ( ( M gcd N ) e. NN0 -> 0 <_ ( M gcd N ) )
5 leltne 
 |-  ( ( 0 e. RR /\ ( M gcd N ) e. RR /\ 0 <_ ( M gcd N ) ) -> ( 0 < ( M gcd N ) <-> ( M gcd N ) =/= 0 ) )
6 2 3 4 5 mp3an2i 
 |-  ( ( M gcd N ) e. NN0 -> ( 0 < ( M gcd N ) <-> ( M gcd N ) =/= 0 ) )
7 1 6 syl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( 0 < ( M gcd N ) <-> ( M gcd N ) =/= 0 ) )
8 gcdeq0 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) = 0 <-> ( M = 0 /\ N = 0 ) ) )
9 8 necon3abid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) =/= 0 <-> -. ( M = 0 /\ N = 0 ) ) )
10 7 9 bitr2d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -. ( M = 0 /\ N = 0 ) <-> 0 < ( M gcd N ) ) )