Theorem nn0ge0i

Description: Nonnegative integers are nonnegative. (Contributed by Raph Levien, 10-Dec-2002)

	Ref	Expression
Hypothesis	nn0ge0i.1	$$⊢N\in {\mathbb{N}}_0$$
Assertion	nn0ge0i	$$⊢0\le N$$

Proof

Step	Hyp	Ref	Expression
1		nn0ge0i.1	$$⊢N\in {\mathbb{N}}_0$$
2		nn0ge0	$$⊢N\in {\mathbb{N}}_0\to 0\le N$$
3	1 2	ax-mp	$$⊢0\le N$$