Theorem nn0negleid

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

	Ref	Expression
Assertion	nn0negleid	⊢ ( 𝐴 ∈ ℕ0 → - 𝐴 ≤ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
2	1	renegcld	⊢ ( 𝐴 ∈ ℕ0 → - 𝐴 ∈ ℝ )
3		0red	⊢ ( 𝐴 ∈ ℕ0 → 0 ∈ ℝ )
4		nn0ge0	⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ 𝐴 )
5	1	le0neg2d	⊢ ( 𝐴 ∈ ℕ0 → ( 0 ≤ 𝐴 ↔ - 𝐴 ≤ 0 ) )
6	4 5	mpbid	⊢ ( 𝐴 ∈ ℕ0 → - 𝐴 ≤ 0 )
7	2 3 1 6 4	letrd	⊢ ( 𝐴 ∈ ℕ0 → - 𝐴 ≤ 𝐴 )