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	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 gcd 0 ) = ( abs ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		0z	⊢ 0 ∈ ℤ
2		gcdcom	⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 gcd 𝑁 ) = ( 𝑁 gcd 0 ) )
3	1 2	mpan	⊢ ( 𝑁 ∈ ℤ → ( 0 gcd 𝑁 ) = ( 𝑁 gcd 0 ) )
4		gcd0id	⊢ ( 𝑁 ∈ ℤ → ( 0 gcd 𝑁 ) = ( abs ‘ 𝑁 ) )
5	3 4	eqtr3d	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 gcd 0 ) = ( abs ‘ 𝑁 ) )