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