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 ( 𝜑𝐴 ∈ ℝ )
sn-addlt0d.b ( 𝜑𝐵 ∈ ℝ )
sn-addlt0d.1 ( 𝜑𝐴 < 0 )
sn-addlt0d.2 ( 𝜑𝐵 < 0 )
Assertion sn-addlt0d ( 𝜑 → ( 𝐴 + 𝐵 ) < 0 )

Proof

Step Hyp Ref Expression
1 sn-addlt0d.a ( 𝜑𝐴 ∈ ℝ )
2 sn-addlt0d.b ( 𝜑𝐵 ∈ ℝ )
3 sn-addlt0d.1 ( 𝜑𝐴 < 0 )
4 sn-addlt0d.2 ( 𝜑𝐵 < 0 )
5 1 2 readdcld ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
6 0red ( 𝜑 → 0 ∈ ℝ )
7 sn-ltaddneg ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 < 0 ↔ ( 𝐴 + 𝐵 ) < 𝐴 ) )
8 2 1 7 syl2anc ( 𝜑 → ( 𝐵 < 0 ↔ ( 𝐴 + 𝐵 ) < 𝐴 ) )
9 4 8 mpbid ( 𝜑 → ( 𝐴 + 𝐵 ) < 𝐴 )
10 5 1 6 9 3 lttrd ( 𝜑 → ( 𝐴 + 𝐵 ) < 0 )