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 \in ℤ \to N \gcd N = \|N\|$

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		0z	$⊢ 0 \in ℤ$
3		gcdaddm	$⊢ (1 \in ℤ \land N \in ℤ \land 0 \in ℤ) \to N \gcd 0 = N \gcd (0 + 1 \cdot N)$
4	1 2 3	mp3an13	$⊢ N \in ℤ \to N \gcd 0 = N \gcd (0 + 1 \cdot N)$
5		gcdid0	$⊢ N \in ℤ \to N \gcd 0 = \|N\|$
6		zcn	$⊢ N \in ℤ \to N \in ℂ$
7		mulid2	$⊢ N \in ℂ \to 1 \cdot N = N$
8	7	oveq2d	$⊢ N \in ℂ \to 0 + 1 \cdot N = 0 + N$
9		addid2	$⊢ N \in ℂ \to 0 + N = N$
10	8 9	eqtrd	$⊢ N \in ℂ \to 0 + 1 \cdot N = N$
11	6 10	syl	$⊢ N \in ℤ \to 0 + 1 \cdot N = N$
12	11	oveq2d	$⊢ N \in ℤ \to N \gcd (0 + 1 \cdot N) = N \gcd N$
13	4 5 12	3eqtr3rd	$⊢ N \in ℤ \to N \gcd N = \|N\|$

Metamath Proof Explorer