Metamath Proof Explorer


Theorem le0neg1

Description: Comparison of a number and its negative to zero. (Contributed by NM, 10-May-2004)

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

Proof

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