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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gcdcl | |
|
2 | 0re | |
|
3 | nn0re | |
|
4 | nn0ge0 | |
|
5 | leltne | |
|
6 | 2 3 4 5 | mp3an2i | |
7 | 1 6 | syl | |
8 | gcdeq0 | |
|
9 | 8 | necon3abid | |
10 | 7 9 | bitr2d | |