Description: Comparison of a number and its negative to zero. (Contributed by NM, 24-Aug-1999)
Ref | Expression | ||
---|---|---|---|
Assertion | le0neg2 | |- ( A e. RR -> ( 0 <_ A <-> -u A <_ 0 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re | |- 0 e. RR |
|
2 | leneg | |- ( ( 0 e. RR /\ A e. RR ) -> ( 0 <_ A <-> -u A <_ -u 0 ) ) |
|
3 | 1 2 | mpan | |- ( A e. RR -> ( 0 <_ A <-> -u A <_ -u 0 ) ) |
4 | neg0 | |- -u 0 = 0 |
|
5 | 4 | breq2i | |- ( -u A <_ -u 0 <-> -u A <_ 0 ) |
6 | 3 5 | bitrdi | |- ( A e. RR -> ( 0 <_ A <-> -u A <_ 0 ) ) |