Metamath Proof Explorer

Theorem gcdabs

Description: The gcd of two integers is the same as that of their absolute values. (Contributed by Paul Chapman, 31-Mar-2011) (Proof shortened by SN, 15-Sep-2024)

Ref Expression
Assertion gcdabs ⊢M∈ℤ∧N∈ℤ→MgcdN=MgcdN

Proof

Step Hyp Ref Expression
1 zabscl ⊢N∈ℤ→N∈ℤ
2 gcdabs1 ⊢M∈ℤ∧N∈ℤ→MgcdN=MgcdN
3 1 2 sylan2 ⊢M∈ℤ∧N∈ℤ→MgcdN=MgcdN
4 gcdabs2 ⊢M∈ℤ∧N∈ℤ→MgcdN=MgcdN
5 3 4 eqtrd ⊢M∈ℤ∧N∈ℤ→MgcdN=MgcdN