Theorem ltaddnegr

Description: Adding a negative number to another number decreases it. (Contributed by AV, 19-Mar-2021)

	Ref	Expression
Assertion	ltaddnegr	|- ( ( A e. RR /\ B e. RR ) -> ( A < 0 <-> ( A + B ) < B ) )

Proof

Step	Hyp	Ref	Expression
1		ltaddneg	|- ( ( A e. RR /\ B e. RR ) -> ( A < 0 <-> ( B + A ) < B ) )
2		recn	|- ( B e. RR -> B e. CC )
3		recn	|- ( A e. RR -> A e. CC )
4		addcom	|- ( ( B e. CC /\ A e. CC ) -> ( B + A ) = ( A + B ) )
5	2 3 4	syl2anr	|- ( ( A e. RR /\ B e. RR ) -> ( B + A ) = ( A + B ) )
6	5	breq1d	|- ( ( A e. RR /\ B e. RR ) -> ( ( B + A ) < B <-> ( A + B ) < B ) )
7	1 6	bitrd	|- ( ( A e. RR /\ B e. RR ) -> ( A < 0 <-> ( A + B ) < B ) )