This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ‘ 𝑁 ) )