Theorem sn-mullt0d

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

	Ref	Expression
Hypotheses	sn-mullt0d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	sn-mullt0d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	sn-mullt0d.1	⊢ ( 𝜑 → 𝐴 < 0 )
	sn-mullt0d.2	⊢ ( 𝜑 → 𝐵 < 0 )
Assertion	sn-mullt0d	⊢ ( 𝜑 → 0 < ( 𝐴 · 𝐵 ) )

Proof

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