Metamath Proof Explorer


Theorem sn-addlt0d

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

Ref Expression
Hypotheses sn-addlt0d.a φ A
sn-addlt0d.b φ B
sn-addlt0d.1 φ A < 0
sn-addlt0d.2 φ B < 0
Assertion sn-addlt0d φ A + B < 0

Proof

Step Hyp Ref Expression
1 sn-addlt0d.a φ A
2 sn-addlt0d.b φ B
3 sn-addlt0d.1 φ A < 0
4 sn-addlt0d.2 φ B < 0
5 1 2 readdcld φ A + B
6 0red φ 0
7 sn-ltaddneg B A B < 0 A + B < A
8 2 1 7 syl2anc φ B < 0 A + B < A
9 4 8 mpbid φ A + B < A
10 5 1 6 9 3 lttrd φ A + B < 0