This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nn0nlt0

Description: A nonnegative integer is not less than zero. (Contributed by NM, 9-May-2004) (Revised by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	nn0nlt0	$⊢ A \in ℕ_{0} \to \neg A < 0$

Step	Hyp	Ref	Expression
1		nn0ge0	$⊢ A \in ℕ_{0} \to 0 \leq A$
2		0re	$⊢ 0 \in ℝ$
3		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
4		lenlt	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 \leq A \leftrightarrow \neg A < 0)$
5	2 3 4	sylancr	$⊢ A \in ℕ_{0} \to (0 \leq A \leftrightarrow \neg A < 0)$
6	1 5	mpbid	$⊢ A \in ℕ_{0} \to \neg A < 0$