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

Proof

Step	Hyp	Ref	Expression
1		zabscl	⊢ ( 𝑁 ∈ ℤ → ( abs ‘ 𝑁 ) ∈ ℤ )
2		gcdabs1	⊢ ( ( 𝑀 ∈ ℤ ∧ ( abs ‘ 𝑁 ) ∈ ℤ ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd ( abs ‘ 𝑁 ) ) )
3	1 2	sylan2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd ( abs ‘ 𝑁 ) ) )
4		gcdabs2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) )
5	3 4	eqtrd	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) )