Metamath Proof Explorer


Theorem leaddle0

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 ABA+BAB0

Proof

Step Hyp Ref Expression
1 leaddsub2 ABAA+BABAA
2 1 3anidm13 ABA+BABAA
3 recn AA
4 3 subidd AAA=0
5 4 adantr ABAA=0
6 5 breq2d ABBAAB0
7 2 6 bitrd ABA+BAB0