Theorem nn0ge0

Description: A nonnegative integer is greater than or equal to zero. (Contributed by NM, 9-May-2004) (Revised by Mario Carneiro, 16-May-2014)

	Ref	Expression
Assertion	nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{N}\vee N=0\right)$$
2		nngt0	$$⊢N\in \mathbb{N}\to 0<N$$
3		id	$$⊢N=0\to N=0$$
4	3	eqcomd	$$⊢N=0\to 0=N$$
5	2 4	orim12i	$$⊢\left(N\in \mathbb{N}\vee N=0\right)\to \left(0<N\vee 0=N\right)$$
6	1 5	sylbi	$$⊢N\in {\mathbb{N}}_0\to \left(0<N\vee 0=N\right)$$
7		0re	$$⊢0\in ℝ$$
8		nn0re	$$⊢N\in {\mathbb{N}}_0\to N\in ℝ$$
9		leloe	$$⊢\left(0\in ℝ\wedge N\in ℝ\right)\to \left(0\le N\leftrightarrow \left(0<N\vee 0=N\right)\right)$$
10	7 8 9	sylancr	$$⊢N\in {\mathbb{N}}_0\to \left(0\le N\leftrightarrow \left(0<N\vee 0=N\right)\right)$$
11	6 10	mpbird	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$