Metamath Proof Explorer


Theorem relt0neg2

Description: Comparison of a real and its negative to zero. Compare lt0neg2 . (Contributed by SN, 13-Feb-2024)

Ref Expression
Assertion relt0neg2 A 0 < A 0 - A < 0

Proof

Step Hyp Ref Expression
1 elre0re A 0
2 id A A
3 reltsub1 0 A A 0 < A 0 - A < A - A
4 1 2 2 3 syl3anc A 0 < A 0 - A < A - A
5 resubid A A - A = 0
6 5 breq2d A 0 - A < A - A 0 - A < 0
7 4 6 bitrd A 0 < A 0 - A < 0