Theorem 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	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 𝑀 gcd 𝑁 ) = ( 𝑀 gcd 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		gcdneg	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 gcd - 𝑀 ) = ( 𝑁 gcd 𝑀 ) )
2	1	ancoms	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 gcd - 𝑀 ) = ( 𝑁 gcd 𝑀 ) )
3		znegcl	⊢ ( 𝑀 ∈ ℤ → - 𝑀 ∈ ℤ )
4		gcdcom	⊢ ( ( - 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 𝑀 gcd 𝑁 ) = ( 𝑁 gcd - 𝑀 ) )
5	3 4	sylan	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 𝑀 gcd 𝑁 ) = ( 𝑁 gcd - 𝑀 ) )
6		gcdcom	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) = ( 𝑁 gcd 𝑀 ) )
7	2 5 6	3eqtr4d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 𝑀 gcd 𝑁 ) = ( 𝑀 gcd 𝑁 ) )