Metamath Proof Explorer


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 MN- MgcdN=MgcdN

Proof

Step Hyp Ref Expression
1 gcdneg NMNgcd- M=NgcdM
2 1 ancoms MNNgcd- M=NgcdM
3 znegcl MM
4 gcdcom MN- MgcdN=Ngcd- M
5 3 4 sylan MN- MgcdN=Ngcd- M
6 gcdcom MNMgcdN=NgcdM
7 2 5 6 3eqtr4d MN- MgcdN=MgcdN