Theorem gcdid

Description: The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011)

	Ref	Expression
Assertion	gcdid	$$⊢N\in \mathbb{Z}\to N\gcd N=\left|N\right|$$

Proof

Step	Hyp	Ref	Expression
1		1z	$$⊢1\in \mathbb{Z}$$
2		0z	$$⊢0\in \mathbb{Z}$$
3		gcdaddm	$$⊢\left(1\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge 0\in \mathbb{Z}\right)\to N\gcd 0=N\gcd \left(0+1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
4	1 2 3	mp3an13	$$⊢N\in \mathbb{Z}\to N\gcd 0=N\gcd \left(0+1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
5		gcdid0	$$⊢N\in \mathbb{Z}\to N\gcd 0=\left|N\right|$$
6		zcn	$$⊢N\in \mathbb{Z}\to N\in ℂ$$
7		mullid	$$⊢N\in ℂ\to 1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N$$
8	7	oveq2d	$$⊢N\in ℂ\to 0+1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=0+N$$
9		addlid	$$⊢N\in ℂ\to 0+N=N$$
10	8 9	eqtrd	$$⊢N\in ℂ\to 0+1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N$$
11	6 10	syl	$$⊢N\in \mathbb{Z}\to 0+1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N$$
12	11	oveq2d	$$⊢N\in \mathbb{Z}\to N\gcd \left(0+1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)=N\gcd N$$
13	4 5 12	3eqtr3rd	$$⊢N\in \mathbb{Z}\to N\gcd N=\left|N\right|$$