Theorem ltaddnegr

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

	Ref	Expression
Assertion	ltaddnegr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<0\leftrightarrow A+B<B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ltaddneg	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<0\leftrightarrow B+A<B\right)$$
2		recn	$$⊢B\in ℝ\to B\in ℂ$$
3		recn	$$⊢A\in ℝ\to A\in ℂ$$
4		addcom	$$⊢\left(B\in ℂ\wedge A\in ℂ\right)\to B+A=A+B$$
5	2 3 4	syl2anr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B+A=A+B$$
6	5	breq1d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B+A<B\leftrightarrow A+B<B\right)$$
7	1 6	bitrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<0\leftrightarrow A+B<B\right)$$