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 ⊢ N ∈ ℤ → N gcd N = N

Proof

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