Metamath Proof Explorer

Theorem gcdabs2

Description: gcd of the absolute value of the second operator. (Contributed by Scott Fenton, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion gcdabs2 ⊢N∈ℤ∧M∈ℤ→NgcdM=NgcdM

Proof

Step Hyp Ref Expression
1 gcdabs1 ⊢M∈ℤ∧N∈ℤ→MgcdN=MgcdN
2 1 ancoms ⊢N∈ℤ∧M∈ℤ→MgcdN=MgcdN
3 zabscl ⊢M∈ℤ→M∈ℤ
4 gcdcom ⊢N∈ℤ∧M∈ℤ→NgcdM=MgcdN
5 3 4 sylan2 ⊢N∈ℤ∧M∈ℤ→NgcdM=MgcdN
6 gcdcom ⊢N∈ℤ∧M∈ℤ→NgcdM=MgcdN
7 2 5 6 3eqtr4d ⊢N∈ℤ∧M∈ℤ→NgcdM=NgcdM