Theorem mullt0b2d

Description: When the second term is negative, the first term is positive iff the product is negative. (Contributed by SN, 26-Nov-2025)

	Ref	Expression
Hypotheses	mullt0b2d.a	$$⊢\phi \to A\in ℝ$$
	mullt0b2d.b	$$⊢\phi \to B\in ℝ$$
	mullt0b2d.1	$$⊢\phi \to B<0$$
Assertion	mullt0b2d	$$⊢\phi \to \left(0<A\leftrightarrow AB<0\right)$$

Proof

Step	Hyp	Ref	Expression
1		mullt0b2d.a	$$⊢\phi \to A\in ℝ$$
2		mullt0b2d.b	$$⊢\phi \to B\in ℝ$$
3		mullt0b2d.1	$$⊢\phi \to B<0$$
4		simpr	$$⊢\left(\phi \wedge 0<A\right)\to 0<A$$
5	4	gt0ne0d	$$⊢\left(\phi \wedge 0<A\right)\to A\ne 0$$
6	3	adantr	$$⊢\left(\phi \wedge 0<A\right)\to B<0$$
7	6	lt0ne0d	$$⊢\left(\phi \wedge 0<A\right)\to B\ne 0$$
8	5 7	jca	$$⊢\left(\phi \wedge 0<A\right)\to \left(A\ne 0\wedge B\ne 0\right)$$
9		neanior	$$⊢\left(A\ne 0\wedge B\ne 0\right)\leftrightarrow \neg \left(A=0\vee B=0\right)$$
10	8 9	sylib	$$⊢\left(\phi \wedge 0<A\right)\to \neg \left(A=0\vee B=0\right)$$
11	1	adantr	$$⊢\left(\phi \wedge 0<A\right)\to A\in ℝ$$
12	2	adantr	$$⊢\left(\phi \wedge 0<A\right)\to B\in ℝ$$
13	11 12	sn-remul0ord	$$⊢\left(\phi \wedge 0<A\right)\to \left(AB=0\leftrightarrow \left(A=0\vee B=0\right)\right)$$
14	10 13	mtbird	$$⊢\left(\phi \wedge 0<A\right)\to \neg AB=0$$
15		0red	$$⊢\phi \to 0\in ℝ$$
16	2 15 3	ltnsymd	$$⊢\phi \to \neg 0<B$$
17	16	adantr	$$⊢\left(\phi \wedge 0<A\right)\to \neg 0<B$$
18	11 12 4	mulgt0b1d	$$⊢\left(\phi \wedge 0<A\right)\to \left(0<B\leftrightarrow 0<AB\right)$$
19	17 18	mtbid	$$⊢\left(\phi \wedge 0<A\right)\to \neg 0<AB$$
20		ioran	$$⊢\neg \left(AB=0\vee 0<AB\right)\leftrightarrow \left(\neg AB=0\wedge \neg 0<AB\right)$$
21	14 19 20	sylanbrc	$$⊢\left(\phi \wedge 0<A\right)\to \neg \left(AB=0\vee 0<AB\right)$$
22	1 2	remulcld	$$⊢\phi \to AB\in ℝ$$
23	22 15	lttrid	$$⊢\phi \to \left(AB<0\leftrightarrow \neg \left(AB=0\vee 0<AB\right)\right)$$
24	23	adantr	$$⊢\left(\phi \wedge 0<A\right)\to \left(AB<0\leftrightarrow \neg \left(AB=0\vee 0<AB\right)\right)$$
25	21 24	mpbird	$$⊢\left(\phi \wedge 0<A\right)\to AB<0$$
26		remul02	$$⊢B\in ℝ\to 0\cdot B=0$$
27	2 26	syl	$$⊢\phi \to 0\cdot B=0$$
28	15	ltnrd	$$⊢\phi \to \neg 0<0$$
29	27 28	eqnbrtrd	$$⊢\phi \to \neg 0\cdot B<0$$
30		oveq1	$$⊢0=A\to 0\cdot B=AB$$
31	30	breq1d	$$⊢0=A\to \left(0\cdot B<0\leftrightarrow AB<0\right)$$
32	31	notbid	$$⊢0=A\to \left(\neg 0\cdot B<0\leftrightarrow \neg AB<0\right)$$
33	29 32	syl5ibcom	$$⊢\phi \to \left(0=A\to \neg AB<0\right)$$
34	33	con2d	$$⊢\phi \to \left(AB<0\to \neg 0=A\right)$$
35	34	imp	$$⊢\left(\phi \wedge AB<0\right)\to \neg 0=A$$
36	16	adantr	$$⊢\left(\phi \wedge AB<0\right)\to \neg 0<B$$
37		simplr	$$⊢\left(\left(\phi \wedge AB<0\right)\wedge A<0\right)\to AB<0$$
38	1	ad2antrr	$$⊢\left(\left(\phi \wedge AB<0\right)\wedge A<0\right)\to A\in ℝ$$
39	2	ad2antrr	$$⊢\left(\left(\phi \wedge AB<0\right)\wedge A<0\right)\to B\in ℝ$$
40		simpr	$$⊢\left(\left(\phi \wedge AB<0\right)\wedge A<0\right)\to A<0$$
41	38 39 40	mullt0b1d	$$⊢\left(\left(\phi \wedge AB<0\right)\wedge A<0\right)\to \left(0<B\leftrightarrow AB<0\right)$$
42	37 41	mpbird	$$⊢\left(\left(\phi \wedge AB<0\right)\wedge A<0\right)\to 0<B$$
43	36 42	mtand	$$⊢\left(\phi \wedge AB<0\right)\to \neg A<0$$
44		ioran	$$⊢\neg \left(0=A\vee A<0\right)\leftrightarrow \left(\neg 0=A\wedge \neg A<0\right)$$
45	35 43 44	sylanbrc	$$⊢\left(\phi \wedge AB<0\right)\to \neg \left(0=A\vee A<0\right)$$
46	15 1	lttrid	$$⊢\phi \to \left(0<A\leftrightarrow \neg \left(0=A\vee A<0\right)\right)$$
47	46	adantr	$$⊢\left(\phi \wedge AB<0\right)\to \left(0<A\leftrightarrow \neg \left(0=A\vee A<0\right)\right)$$
48	45 47	mpbird	$$⊢\left(\phi \wedge AB<0\right)\to 0<A$$
49	25 48	impbida	$$⊢\phi \to \left(0<A\leftrightarrow AB<0\right)$$