Theorem gcdabs1

Description: gcd of the absolute value of the first operator. (Contributed by Scott Fenton, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	gcdabs1	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( abs ‘ 𝑁 ) gcd 𝑀 ) = ( 𝑁 gcd 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( ( abs ‘ 𝑁 ) = 𝑁 → ( ( abs ‘ 𝑁 ) gcd 𝑀 ) = ( 𝑁 gcd 𝑀 ) )
2	1	a1i	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( abs ‘ 𝑁 ) = 𝑁 → ( ( abs ‘ 𝑁 ) gcd 𝑀 ) = ( 𝑁 gcd 𝑀 ) ) )
3		neggcd	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( - 𝑁 gcd 𝑀 ) = ( 𝑁 gcd 𝑀 ) )
4		oveq1	⊢ ( ( abs ‘ 𝑁 ) = - 𝑁 → ( ( abs ‘ 𝑁 ) gcd 𝑀 ) = ( - 𝑁 gcd 𝑀 ) )
5	4	eqeq1d	⊢ ( ( abs ‘ 𝑁 ) = - 𝑁 → ( ( ( abs ‘ 𝑁 ) gcd 𝑀 ) = ( 𝑁 gcd 𝑀 ) ↔ ( - 𝑁 gcd 𝑀 ) = ( 𝑁 gcd 𝑀 ) ) )
6	3 5	syl5ibrcom	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( abs ‘ 𝑁 ) = - 𝑁 → ( ( abs ‘ 𝑁 ) gcd 𝑀 ) = ( 𝑁 gcd 𝑀 ) ) )
7		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
8	7	absord	⊢ ( 𝑁 ∈ ℤ → ( ( abs ‘ 𝑁 ) = 𝑁 ∨ ( abs ‘ 𝑁 ) = - 𝑁 ) )
9	8	adantr	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( abs ‘ 𝑁 ) = 𝑁 ∨ ( abs ‘ 𝑁 ) = - 𝑁 ) )
10	2 6 9	mpjaod	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( abs ‘ 𝑁 ) gcd 𝑀 ) = ( 𝑁 gcd 𝑀 ) )