Theorem nn0le0eq0

Description: A nonnegative integer is less than or equal to zero iff it is equal to zero. (Contributed by NM, 9-Dec-2005)

	Ref	Expression
Assertion	nn0le0eq0	$$⊢N\in {\mathbb{N}}_0\to \left(N\le 0\leftrightarrow N=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
2	1	biantrud	$$⊢N\in {\mathbb{N}}_0\to \left(N\le 0\leftrightarrow \left(N\le 0\wedge 0\le N\right)\right)$$
3		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
4		0re	$$⊢0\in ℝ$$
5		letri3	$$⊢\left(N\in ℝ\wedge 0\in ℝ\right)\to \left(N=0\leftrightarrow \left(N\le 0\wedge 0\le N\right)\right)$$
6	3 4 5	sylancl	$$⊢N\in {\mathbb{N}}_0\to \left(N=0\leftrightarrow \left(N\le 0\wedge 0\le N\right)\right)$$
7	2 6	bitr4d	$$⊢N\in {\mathbb{N}}_0\to \left(N\le 0\leftrightarrow N=0\right)$$