Theorem sn-addlt0d

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

	Ref	Expression
Hypotheses	sn-addlt0d.a	|- ( ph -> A e. RR )
	sn-addlt0d.b	|- ( ph -> B e. RR )
	sn-addlt0d.1	|- ( ph -> A < 0 )
	sn-addlt0d.2	|- ( ph -> B < 0 )
Assertion	sn-addlt0d	|- ( ph -> ( A + B ) < 0 )

Proof

Step	Hyp	Ref	Expression
1		sn-addlt0d.a	|- ( ph -> A e. RR )
2		sn-addlt0d.b	|- ( ph -> B e. RR )
3		sn-addlt0d.1	|- ( ph -> A < 0 )
4		sn-addlt0d.2	|- ( ph -> B < 0 )
5	1 2	readdcld	|- ( ph -> ( A + B ) e. RR )
6		0red	|- ( ph -> 0 e. RR )
7		sn-ltaddneg	|- ( ( B e. RR /\ A e. RR ) -> ( B < 0 <-> ( A + B ) < A ) )
8	2 1 7	syl2anc	|- ( ph -> ( B < 0 <-> ( A + B ) < A ) )
9	4 8	mpbid	|- ( ph -> ( A + B ) < A )
10	5 1 6 9 3	lttrd	|- ( ph -> ( A + B ) < 0 )