# 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 ${⊢}0\mathrm{gcd}0=0$

### Proof

Step Hyp Ref Expression
1 0z ${⊢}0\in ℤ$
2 gcdval ${⊢}\left(0\in ℤ\wedge 0\in ℤ\right)\to 0\mathrm{gcd}0=if\left(\left(0=0\wedge 0=0\right),0,sup\left(\left\{{n}\in ℤ|\left({n}\parallel 0\wedge {n}\parallel 0\right)\right\},ℝ,<\right)\right)$
3 1 1 2 mp2an ${⊢}0\mathrm{gcd}0=if\left(\left(0=0\wedge 0=0\right),0,sup\left(\left\{{n}\in ℤ|\left({n}\parallel 0\wedge {n}\parallel 0\right)\right\},ℝ,<\right)\right)$
4 eqid ${⊢}0=0$
5 iftrue ${⊢}\left(0=0\wedge 0=0\right)\to if\left(\left(0=0\wedge 0=0\right),0,sup\left(\left\{{n}\in ℤ|\left({n}\parallel 0\wedge {n}\parallel 0\right)\right\},ℝ,<\right)\right)=0$
6 4 4 5 mp2an ${⊢}if\left(\left(0=0\wedge 0=0\right),0,sup\left(\left\{{n}\in ℤ|\left({n}\parallel 0\wedge {n}\parallel 0\right)\right\},ℝ,<\right)\right)=0$
7 3 6 eqtri ${⊢}0\mathrm{gcd}0=0$