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 ) |
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 ) |