This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 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 𝑀 ) )