Theorem mulltgt0d

Description: Negative times positive is negative. (Contributed by SN, 26-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		mullt0b1d.a	$$⊢\phi \to A\in ℝ$$
2		mullt0b1d.b	$$⊢\phi \to B\in ℝ$$
3		mullt0b1d.1	$$⊢\phi \to A<0$$
4		mulltgt0d.2	$$⊢\phi \to 0<B$$
5	3	lt0ne0d	$$⊢\phi \to A\ne 0$$
6	4	gt0ne0d	$$⊢\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		0red	$$⊢\phi \to 0\in ℝ$$
13	1 12 3	ltnsymd	$$⊢\phi \to \neg 0<A$$
14	1 2 4	mulgt0b2d	$$⊢\phi \to \left(0<A\leftrightarrow 0<AB\right)$$
15	13 14	mtbid	$$⊢\phi \to \neg 0<AB$$
16		ioran	$$⊢\neg \left(AB=0\vee 0<AB\right)\leftrightarrow \left(\neg AB=0\wedge \neg 0<AB\right)$$
17	11 15 16	sylanbrc	$$⊢\phi \to \neg \left(AB=0\vee 0<AB\right)$$
18	1 2	remulcld	$$⊢\phi \to AB\in ℝ$$
19	18 12	lttrid	$$⊢\phi \to \left(AB<0\leftrightarrow \neg \left(AB=0\vee 0<AB\right)\right)$$
20	17 19	mpbird	$$⊢\phi \to AB<0$$