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

Metamath Proof Explorer

Theorem nn0negleid

Description: A nonnegative integer is greater than or equal to its negative. (Contributed by AV, 13-Aug-2021)

		Ref	Expression
	Assertion	nn0negleid	$⊢ A \in ℕ_{0} \to - A \leq A$

Step	Hyp	Ref	Expression
1		nn0re	$⊢ A \in ℕ_{0} \to A \in ℝ$
2	1	renegcld	$⊢ A \in ℕ_{0} \to - A \in ℝ$
3		0red	$⊢ A \in ℕ_{0} \to 0 \in ℝ$
4		nn0ge0	$⊢ A \in ℕ_{0} \to 0 \leq A$
5	1	le0neg2d	$⊢ A \in ℕ_{0} \to (0 \leq A \leftrightarrow - A \leq 0)$
6	4 5	mpbid	$⊢ A \in ℕ_{0} \to - A \leq 0$
7	2 3 1 6 4	letrd	$⊢ A \in ℕ_{0} \to - A \leq A$