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	$$⊢\left(N\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to \left|N\right|\gcd M=N\gcd M$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢\left|N\right|=N\to \left|N\right|\gcd M=N\gcd M$$
2	1	a1i	$$⊢\left(N\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to \left(\left|N\right|=N\to \left|N\right|\gcd M=N\gcd M\right)$$
3		neggcd	$$⊢\left(N\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to \mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\gcd M=N\gcd M$$
4		oveq1	$$⊢\left|N\right|=-N\to \left|N\right|\gcd M=\mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\gcd M$$
5	4	eqeq1d	$$⊢\left|N\right|=-N\to \left(\left|N\right|\gcd M=N\gcd M\leftrightarrow \mathrm{-\; <mi\; mathcolor="\#808">N</mi>}\gcd M=N\gcd M\right)$$
6	3 5	syl5ibrcom	$$⊢\left(N\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to \left(\left|N\right|=-N\to \left|N\right|\gcd M=N\gcd M\right)$$
7		zre	$$⊢N\in \mathbb{Z}\to N\in ℝ$$
8	7	absord	$$⊢N\in \mathbb{Z}\to \left(\left|N\right|=N\vee \left|N\right|=-N\right)$$
9	8	adantr	$$⊢\left(N\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to \left(\left|N\right|=N\vee \left|N\right|=-N\right)$$
10	2 6 9	mpjaod	$$⊢\left(N\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to \left|N\right|\gcd M=N\gcd M$$