Description: The sum of negative numbers is negative. (Contributed by SN, 25-Jan-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sn-addlt0d.a | ||
sn-addlt0d.b | |||
sn-addlt0d.1 | |||
sn-addlt0d.2 | |||
Assertion | sn-addlt0d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sn-addlt0d.a | ||
2 | sn-addlt0d.b | ||
3 | sn-addlt0d.1 | ||
4 | sn-addlt0d.2 | ||
5 | 1 2 | readdcld | |
6 | 0red | ||
7 | sn-ltaddneg | ||
8 | 2 1 7 | syl2anc | |
9 | 4 8 | mpbid | |
10 | 5 1 6 9 3 | lttrd |