Theorem ltaddneg

Description: Adding a negative number to another number decreases it. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2		ltadd2	$$⊢\left(A\in ℝ\wedge 0\in ℝ\wedge B\in ℝ\right)\to \left(A<0\leftrightarrow B+A<B+0\right)$$
3	1 2	mp3an2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<0\leftrightarrow B+A<B+0\right)$$
4		recn	$$⊢B\in ℝ\to B\in ℂ$$
5	4	addid1d	$$⊢B\in ℝ\to B+0=B$$
6	5	adantl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B+0=B$$
7	6	breq2d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(B+A<B+0\leftrightarrow B+A<B\right)$$
8	3 7	bitrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<0\leftrightarrow B+A<B\right)$$