Metamath Proof Explorer


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 mulid2 ( 𝑁 ∈ ℂ → ( 1 · 𝑁 ) = 𝑁 )
8 7 oveq2d ( 𝑁 ∈ ℂ → ( 0 + ( 1 · 𝑁 ) ) = ( 0 + 𝑁 ) )
9 addid2 ( 𝑁 ∈ ℂ → ( 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 ‘ 𝑁 ) )