Theorem sn-addlt0d

Description: The sum of negative numbers is negative. (Contributed by SN, 25-Jan-2025)

	Ref	Expression
Hypotheses	sn-addlt0d.a	$$⊢\phi \to A\in ℝ$$
	sn-addlt0d.b	$$⊢\phi \to B\in ℝ$$
	sn-addlt0d.1	$$⊢\phi \to A<0$$
	sn-addlt0d.2	$$⊢\phi \to B<0$$
Assertion	sn-addlt0d	$$⊢\phi \to A+B<0$$

Proof

Step	Hyp	Ref	Expression
1		sn-addlt0d.a	$$⊢\phi \to A\in ℝ$$
2		sn-addlt0d.b	$$⊢\phi \to B\in ℝ$$
3		sn-addlt0d.1	$$⊢\phi \to A<0$$
4		sn-addlt0d.2	$$⊢\phi \to B<0$$
5	1 2	readdcld	$$⊢\phi \to A+B\in ℝ$$
6		0red	$$⊢\phi \to 0\in ℝ$$
7		sn-ltaddneg	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \left(B<0\leftrightarrow A+B<A\right)$$
8	2 1 7	syl2anc	$$⊢\phi \to \left(B<0\leftrightarrow A+B<A\right)$$
9	4 8	mpbid	$$⊢\phi \to A+B<A$$
10	5 1 6 9 3	lttrd	$$⊢\phi \to A+B<0$$