Description: Extended real version of lt0neg1 . (Contributed by Mario Carneiro, 20-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | xlt0neg1 | |- ( A e. RR* -> ( A < 0 <-> 0 < -e A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0xr | |- 0 e. RR* |
|
2 | xltneg | |- ( ( A e. RR* /\ 0 e. RR* ) -> ( A < 0 <-> -e 0 < -e A ) ) |
|
3 | 1 2 | mpan2 | |- ( A e. RR* -> ( A < 0 <-> -e 0 < -e A ) ) |
4 | xneg0 | |- -e 0 = 0 |
|
5 | 4 | breq1i | |- ( -e 0 < -e A <-> 0 < -e A ) |
6 | 3 5 | bitrdi | |- ( A e. RR* -> ( A < 0 <-> 0 < -e A ) ) |