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

Proof

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