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 A 0 < A A < 0

Proof

Step Hyp Ref Expression
1 0re 0
2 ltneg 0 A 0 < A A < 0
3 1 2 mpan A 0 < A A < 0
4 neg0 0 = 0
5 4 breq2i A < 0 A < 0
6 3 5 syl6bb A 0 < A A < 0