Description: Comparison of a real and its negative to zero. Compare lt0neg2 . (Contributed by SN, 13-Feb-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | relt0neg2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elre0re | ||
2 | id | ||
3 | reltsub1 | ||
4 | 1 2 2 3 | syl3anc | |
5 | resubid | ||
6 | 5 | breq2d | |
7 | 4 6 | bitrd |