Description: The sum of a real number and a second real number is less than the real number iff the second real number is negative. (Contributed by Alexander van der Vekens, 30-May-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | leaddle0 | |- ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) <_ A <-> B <_ 0 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | leaddsub2 | |- ( ( A e. RR /\ B e. RR /\ A e. RR ) -> ( ( A + B ) <_ A <-> B <_ ( A - A ) ) ) |
|
| 2 | 1 | 3anidm13 | |- ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) <_ A <-> B <_ ( A - A ) ) ) |
| 3 | recn | |- ( A e. RR -> A e. CC ) |
|
| 4 | 3 | subidd | |- ( A e. RR -> ( A - A ) = 0 ) |
| 5 | 4 | adantr | |- ( ( A e. RR /\ B e. RR ) -> ( A - A ) = 0 ) |
| 6 | 5 | breq2d | |- ( ( A e. RR /\ B e. RR ) -> ( B <_ ( A - A ) <-> B <_ 0 ) ) |
| 7 | 2 6 | bitrd | |- ( ( A e. RR /\ B e. RR ) -> ( ( A + B ) <_ A <-> B <_ 0 ) ) |