Metamath Proof Explorer


Theorem gcd0val

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 0gcd0=0

Proof

Step Hyp Ref Expression
1 0z 0
2 gcdval 000gcd0=if0=00=00supn|n0n0<
3 1 1 2 mp2an 0gcd0=if0=00=00supn|n0n0<
4 eqid 0=0
5 iftrue 0=00=0if0=00=00supn|n0n0<=0
6 4 4 5 mp2an if0=00=00supn|n0n0<=0
7 3 6 eqtri 0gcd0=0