This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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