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

Metamath Proof Explorer

Theorem sn-mullt0d

Description: The product of two negative numbers is positive. (Contributed by SN, 1-Dec-2025)

Ref Expression
Hypotheses sn-mullt0d.a ⊢ φ → A ∈ ℝ
sn-mullt0d.b ⊢ φ → B ∈ ℝ
sn-mullt0d.1 ⊢ φ → A < 0
sn-mullt0d.2 ⊢ φ → B < 0
Assertion sn-mullt0d ⊢ φ → 0 < A ⁢ B

Proof

Step Hyp Ref Expression
1 sn-mullt0d.a ⊢ φ → A ∈ ℝ
2 sn-mullt0d.b ⊢ φ → B ∈ ℝ
3 sn-mullt0d.1 ⊢ φ → A < 0
4 sn-mullt0d.2 ⊢ φ → B < 0
5 3 lt0ne0d ⊢ φ → A ≠ 0
6 4 lt0ne0d ⊢ φ → B ≠ 0
7 5 6 jca ⊢ φ → A ≠ 0 ∧ B ≠ 0
8 neanior ⊢ A ≠ 0 ∧ B ≠ 0 ↔ ¬ A = 0 ∨ B = 0
9 7 8 sylib ⊢ φ → ¬ A = 0 ∨ B = 0
10 1 2 sn-remul0ord ⊢ φ → A ⁢ B = 0 ↔ A = 0 ∨ B = 0
11 9 10 mtbird ⊢ φ → ¬ A ⁢ B = 0
12 11 neqcomd ⊢ φ → ¬ 0 = A ⁢ B
13 0red ⊢ φ → 0 ∈ ℝ
14 2 13 4 ltnsymd ⊢ φ → ¬ 0 < B
15 1 2 3 mullt0b1d ⊢ φ → 0 < B ↔ A ⁢ B < 0
16 14 15 mtbid ⊢ φ → ¬ A ⁢ B < 0
17 ioran ⊢ ¬ 0 = A ⁢ B ∨ A ⁢ B < 0 ↔ ¬ 0 = A ⁢ B ∧ ¬ A ⁢ B < 0
18 12 16 17 sylanbrc ⊢ φ → ¬ 0 = A ⁢ B ∨ A ⁢ B < 0
19 1 2 remulcld ⊢ φ → A ⁢ B ∈ ℝ
20 13 19 lttrid ⊢ φ → 0 < A ⁢ B ↔ ¬ 0 = A ⁢ B ∨ A ⁢ B < 0
21 18 20 mpbird ⊢ φ → 0 < A ⁢ B