neggcd

Description: Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011)

		Ref	Expression
	Assertion	neggcd	$⊢ (M \in ℤ \land N \in ℤ) \to -M \gcd N = M \gcd N$

Step	Hyp	Ref	Expression
1		gcdneg	$⊢ (N \in ℤ \land M \in ℤ) \to N \gcd -M = N \gcd M$
2	1	ancoms	$⊢ (M \in ℤ \land N \in ℤ) \to N \gcd -M = N \gcd M$
3		znegcl	$⊢ M \in ℤ \to - M \in ℤ$
4		gcdcom	$⊢ (- M \in ℤ \land N \in ℤ) \to -M \gcd N = N \gcd -M$
5	3 4	sylan	$⊢ (M \in ℤ \land N \in ℤ) \to -M \gcd N = N \gcd -M$
6		gcdcom	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N = N \gcd M$
7	2 5 6	3eqtr4d	$⊢ (M \in ℤ \land N \in ℤ) \to -M \gcd N = M \gcd N$

Metamath Proof Explorer