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