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	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 gcd ( abs ‘ 𝑀 ) ) = ( 𝑁 gcd 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		gcdabs1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) gcd 𝑁 ) = ( 𝑀 gcd 𝑁 ) )
2	1	ancoms	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) gcd 𝑁 ) = ( 𝑀 gcd 𝑁 ) )
3		zabscl	⊢ ( 𝑀 ∈ ℤ → ( abs ‘ 𝑀 ) ∈ ℤ )
4		gcdcom	⊢ ( ( 𝑁 ∈ ℤ ∧ ( abs ‘ 𝑀 ) ∈ ℤ ) → ( 𝑁 gcd ( abs ‘ 𝑀 ) ) = ( ( abs ‘ 𝑀 ) gcd 𝑁 ) )
5	3 4	sylan2	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 gcd ( abs ‘ 𝑀 ) ) = ( ( abs ‘ 𝑀 ) gcd 𝑁 ) )
6		gcdcom	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 gcd 𝑀 ) = ( 𝑀 gcd 𝑁 ) )
7	2 5 6	3eqtr4d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 gcd ( abs ‘ 𝑀 ) ) = ( 𝑁 gcd 𝑀 ) )