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 MN¬M=0N=00<MgcdN

Proof

Step Hyp Ref Expression
1 gcdcl MNMgcdN0
2 0re 0
3 nn0re MgcdN0MgcdN
4 nn0ge0 MgcdN00MgcdN
5 leltne 0MgcdN0MgcdN0<MgcdNMgcdN0
6 2 3 4 5 mp3an2i MgcdN00<MgcdNMgcdN0
7 1 6 syl MN0<MgcdNMgcdN0
8 gcdeq0 MNMgcdN=0M=0N=0
9 8 necon3abid MNMgcdN0¬M=0N=0
10 7 9 bitr2d MN¬M=0N=00<MgcdN