Theorem sn-mullt0d

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

	Ref	Expression
Hypotheses	sn-mullt0d.a	$$⊢\phi \to A\in ℝ$$
	sn-mullt0d.b	$$⊢\phi \to B\in ℝ$$
	sn-mullt0d.1	$$⊢\phi \to A<0$$
	sn-mullt0d.2	$$⊢\phi \to B<0$$
Assertion	sn-mullt0d	$$⊢\phi \to 0<AB$$

Proof

Step	Hyp	Ref	Expression
1		sn-mullt0d.a	$$⊢\phi \to A\in ℝ$$
2		sn-mullt0d.b	$$⊢\phi \to B\in ℝ$$
3		sn-mullt0d.1	$$⊢\phi \to A<0$$
4		sn-mullt0d.2	$$⊢\phi \to B<0$$
5	3	lt0ne0d	$$⊢\phi \to A\ne 0$$
6	4	lt0ne0d	$$⊢\phi \to B\ne 0$$
7	5 6	jca	$$⊢\phi \to \left(A\ne 0\wedge B\ne 0\right)$$
8		neanior	$$⊢\left(A\ne 0\wedge B\ne 0\right)\leftrightarrow \neg \left(A=0\vee B=0\right)$$
9	7 8	sylib	$$⊢\phi \to \neg \left(A=0\vee B=0\right)$$
10	1 2	sn-remul0ord	$$⊢\phi \to \left(AB=0\leftrightarrow \left(A=0\vee B=0\right)\right)$$
11	9 10	mtbird	$$⊢\phi \to \neg AB=0$$
12	11	neqcomd	$$⊢\phi \to \neg 0=AB$$
13		0red	$$⊢\phi \to 0\in ℝ$$
14	2 13 4	ltnsymd	$$⊢\phi \to \neg 0<B$$
15	1 2 3	mullt0b1d	$$⊢\phi \to \left(0<B\leftrightarrow AB<0\right)$$
16	14 15	mtbid	$$⊢\phi \to \neg AB<0$$
17		ioran	$$⊢\neg \left(0=AB\vee AB<0\right)\leftrightarrow \left(\neg 0=AB\wedge \neg AB<0\right)$$
18	12 16 17	sylanbrc	$$⊢\phi \to \neg \left(0=AB\vee AB<0\right)$$
19	1 2	remulcld	$$⊢\phi \to AB\in ℝ$$
20	13 19	lttrid	$$⊢\phi \to \left(0<AB\leftrightarrow \neg \left(0=AB\vee AB<0\right)\right)$$
21	18 20	mpbird	$$⊢\phi \to 0<AB$$