Theorem gcdid0

Description: The gcd of an integer and 0 is the integer's absolute value. Theorem 1.4(d)2 in ApostolNT p. 16. (Contributed by Paul Chapman, 31-Mar-2011)

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

Proof

Step	Hyp	Ref	Expression
1		0z	$$⊢0\in \mathbb{Z}$$
2		gcdcom	$$⊢\left(0\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to 0\gcd N=N\gcd 0$$
3	1 2	mpan	$$⊢N\in \mathbb{Z}\to 0\gcd N=N\gcd 0$$
4		gcd0id	$$⊢N\in \mathbb{Z}\to 0\gcd N=\left|N\right|$$
5	3 4	eqtr3d	$$⊢N\in \mathbb{Z}\to N\gcd 0=\left|N\right|$$