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 {\mathbb{N}}_0\to -A\le A$$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
2	1	renegcld	$$⊢A\in {\mathbb{N}}_0\to -A\in ℝ$$
3		0red	$$⊢A\in {\mathbb{N}}_0\to 0\in ℝ$$
4		nn0ge0	$$⊢A\in {\mathbb{N}}_0\to 0\le A$$
5	1	le0neg2d	$$⊢A\in {\mathbb{N}}_0\to \left(0\le A\leftrightarrow -A\le 0\right)$$
6	4 5	mpbid	$$⊢A\in {\mathbb{N}}_0\to -A\le 0$$
7	2 3 1 6 4	letrd	$$⊢A\in {\mathbb{N}}_0\to -A\le A$$