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 {\mathbb{N}}_0\to N\gcd 0=N$$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
2		gcdid0	$$⊢N\in \mathbb{Z}\to N\gcd 0=\left|N\right|$$
3	1 2	syl	$$⊢N\in {\mathbb{N}}_0\to N\gcd 0=\left|N\right|$$
4		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
5		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
6	4 5	absidd	$$⊢N\in {\mathbb{N}}_0\to \left|N\right|=N$$
7	3 6	eqtrd	$$⊢N\in {\mathbb{N}}_0\to N\gcd 0=N$$