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

Proof

Step	Hyp	Ref	Expression
1		1z	⊢ 1 ∈ ℤ
2		0z	⊢ 0 ∈ ℤ
3		gcdaddm	⊢ ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 𝑁 gcd 0 ) = ( 𝑁 gcd ( 0 + ( 1 · 𝑁 ) ) ) )
4	1 2 3	mp3an13	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 gcd 0 ) = ( 𝑁 gcd ( 0 + ( 1 · 𝑁 ) ) ) )
5		gcdid0	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 gcd 0 ) = ( abs ‘ 𝑁 ) )
6		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
7		mullid	⊢ ( 𝑁 ∈ ℂ → ( 1 · 𝑁 ) = 𝑁 )
8	7	oveq2d	⊢ ( 𝑁 ∈ ℂ → ( 0 + ( 1 · 𝑁 ) ) = ( 0 + 𝑁 ) )
9		addlid	⊢ ( 𝑁 ∈ ℂ → ( 0 + 𝑁 ) = 𝑁 )
10	8 9	eqtrd	⊢ ( 𝑁 ∈ ℂ → ( 0 + ( 1 · 𝑁 ) ) = 𝑁 )
11	6 10	syl	⊢ ( 𝑁 ∈ ℤ → ( 0 + ( 1 · 𝑁 ) ) = 𝑁 )
12	11	oveq2d	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 gcd ( 0 + ( 1 · 𝑁 ) ) ) = ( 𝑁 gcd 𝑁 ) )
13	4 5 12	3eqtr3rd	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 gcd 𝑁 ) = ( abs ‘ 𝑁 ) )