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\gcd 0=0$$

Proof

Step	Hyp	Ref	Expression
1		0z	$$⊢0\in \mathbb{Z}$$
2		gcdval	$$⊢\left(0\in \mathbb{Z}\wedge 0\in \mathbb{Z}\right)\to 0\gcd 0=if\left(\left(0=0\wedge 0=0\right),0,sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel 0\wedge n\parallel 0\right)\right\},ℝ,<\right)\right)$$
3	1 1 2	mp2an	$$⊢0\gcd 0=if\left(\left(0=0\wedge 0=0\right),0,sup\left(\left\{n\in \mathbb{Z}|\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 \mathbb{Z}|\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 \mathbb{Z}|\left(n\parallel 0\wedge n\parallel 0\right)\right\},ℝ,<\right)\right)=0$$
7	3 6	eqtri	$$⊢0\gcd 0=0$$