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 ℕ_{0} \to 0 \leq N$

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		nngt0	$⊢ N \in ℕ \to 0 < N$
3		id	$⊢ N = 0 \to N = 0$
4	3	eqcomd	$⊢ N = 0 \to 0 = N$
5	2 4	orim12i	$⊢ (N \in ℕ \lor N = 0) \to (0 < N \lor 0 = N)$
6	1 5	sylbi	$⊢ N \in ℕ_{0} \to (0 < N \lor 0 = N)$
7		0re	$⊢ 0 \in ℝ$
8		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
9		leloe	$⊢ (0 \in ℝ \land N \in ℝ) \to (0 \leq N \leftrightarrow (0 < N \lor 0 = N))$
10	7 8 9	sylancr	$⊢ N \in ℕ_{0} \to (0 \leq N \leftrightarrow (0 < N \lor 0 = N))$
11	6 10	mpbird	$⊢ N \in ℕ_{0} \to 0 \leq N$

Metamath Proof Explorer