This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∈ ℝ → A < 0 ↔ 0 < − A

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 ltneg ⊢ A ∈ ℝ ∧ 0 ∈ ℝ → A < 0 ↔ − 0 < − A
3 1 2 mpan2 ⊢ A ∈ ℝ → A < 0 ↔ − 0 < − A
4 neg0 ⊢ − 0 = 0
5 4 breq1i ⊢ − 0 < − A ↔ 0 < − A
6 3 5 bitrdi ⊢ A ∈ ℝ → A < 0 ↔ 0 < − A