Description: The value, by convention, of the gcd operator when both operands are 0. (Contributed by Paul Chapman, 21-Mar-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | gcd0val | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0z | |
|
2 | gcdval | |
|
3 | 1 1 2 | mp2an | |
4 | eqid | |
|
5 | iftrue | |
|
6 | 4 4 5 | mp2an | |
7 | 3 6 | eqtri | |