Metamath Proof Explorer


Theorem lt0neg2

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

Ref Expression
Assertion lt0neg2 ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ - 𝐴 < 0 ) )

Proof

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