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 ∈ ℤ → M gcd N = M gcd N

Proof

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