Metamath Proof Explorer


Theorem le0neg2

Description: Comparison of a number and its negative to zero. (Contributed by NM, 24-Aug-1999)

Ref Expression
Assertion le0neg2 ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ - 𝐴 ≤ 0 ) )

Proof

Step Hyp Ref Expression
1 0re 0 ∈ ℝ
2 leneg ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐴 ↔ - 𝐴 ≤ - 0 ) )
3 1 2 mpan ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ - 𝐴 ≤ - 0 ) )
4 neg0 - 0 = 0
5 4 breq2i ( - 𝐴 ≤ - 0 ↔ - 𝐴 ≤ 0 )
6 3 5 bitrdi ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ - 𝐴 ≤ 0 ) )