gcdn0val

Description: The value of the gcd operator when at least one operand is nonzero. (Contributed by Paul Chapman, 21-Mar-2011)

		Ref	Expression
	Assertion	gcdn0val	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd N = sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)$

Step	Hyp	Ref	Expression
1		gcdval	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N = if ((M = 0 \land N = 0), 0, sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <))$
2		iffalse	$⊢ \neg (M = 0 \land N = 0) \to if ((M = 0 \land N = 0), 0, sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)) = sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)$
3	1 2	sylan9eq	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd N = sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)$

Metamath Proof Explorer