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

Metamath Proof Explorer

Theorem nn0gcdid0

Description: The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011)

		Ref	Expression
	Assertion	nn0gcdid0	$⊢ N \in ℕ_{0} \to N \gcd 0 = N$

Step	Hyp	Ref	Expression
1		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
2		gcdid0	$⊢ N \in ℤ \to N \gcd 0 = \|N\|$
3	1 2	syl	$⊢ N \in ℕ_{0} \to N \gcd 0 = \|N\|$
4		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
5		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
6	4 5	absidd	$⊢ N \in ℕ_{0} \to \|N\| = N$
7	3 6	eqtrd	$⊢ N \in ℕ_{0} \to N \gcd 0 = N$