Metamath Proof Explorer


Theorem lt0neg1

Description: Comparison of a number and its negative to zero. Theorem I.23 of Apostol p. 20. (Contributed by NM, 14-May-1999)

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

Proof

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