Theorem gcdnn0id

Description: The gcd of a nonnegative integer and itself is the integer. (Contributed by SN, 25-Aug-2024)

	Ref	Expression
Assertion	gcdnn0id	$$⊢N\in {\mathbb{N}}_0\to N\gcd N=N$$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
2		gcdid	$$⊢N\in \mathbb{Z}\to N\gcd N=\left|N\right|$$
3	1 2	syl	$$⊢N\in {\mathbb{N}}_0\to N\gcd N=\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 N=N$$