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$

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

Metamath Proof Explorer