Theorem mullt0b1d

Description: When the first term is negative, the second term is positive iff the product 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$$
Assertion	mullt0b1d	$$⊢\phi \to \left(0<B\leftrightarrow AB<0\right)$$

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	1	adantr	$$⊢\left(\phi \wedge 0<B\right)\to A\in ℝ$$
5	2	adantr	$$⊢\left(\phi \wedge 0<B\right)\to B\in ℝ$$
6	3	adantr	$$⊢\left(\phi \wedge 0<B\right)\to A<0$$
7		simpr	$$⊢\left(\phi \wedge 0<B\right)\to 0<B$$
8	4 5 6 7	mulltgt0d	$$⊢\left(\phi \wedge 0<B\right)\to AB<0$$
9	3	lt0ne0d	$$⊢\phi \to A\ne 0$$
10	1 9	sn-rereccld	$$⊢\phi \to 1{/}_{ℝ}A\in ℝ$$
11	1 2	remulcld	$$⊢\phi \to AB\in ℝ$$
12	10 11	remulneg2d	$$⊢\phi \to \left(1{/}_{ℝ}A\right)\left(0{-}_{ℝ}AB\right)=0{-}_{ℝ}\left(1{/}_{ℝ}A\right)AB$$
13	1 9	rerecid2d	$$⊢\phi \to \left(1{/}_{ℝ}A\right)A=1$$
14	13	oveq1d	$$⊢\phi \to \left(1{/}_{ℝ}A\right)AB=1B$$
15	10	recnd	$$⊢\phi \to 1{/}_{ℝ}A\in ℂ$$
16	1	recnd	$$⊢\phi \to A\in ℂ$$
17	2	recnd	$$⊢\phi \to B\in ℂ$$
18	15 16 17	mulassd	$$⊢\phi \to \left(1{/}_{ℝ}A\right)AB=\left(1{/}_{ℝ}A\right)AB$$
19		remullid	$$⊢B\in ℝ\to 1B=B$$
20	2 19	syl	$$⊢\phi \to 1B=B$$
21	14 18 20	3eqtr3d	$$⊢\phi \to \left(1{/}_{ℝ}A\right)AB=B$$
22	21	oveq2d	$$⊢\phi \to 0{-}_{ℝ}\left(1{/}_{ℝ}A\right)AB=0{-}_{ℝ}B$$
23	12 22	eqtrd	$$⊢\phi \to \left(1{/}_{ℝ}A\right)\left(0{-}_{ℝ}AB\right)=0{-}_{ℝ}B$$
24	23	adantr	$$⊢\left(\phi \wedge 0<0{-}_{ℝ}AB\right)\to \left(1{/}_{ℝ}A\right)\left(0{-}_{ℝ}AB\right)=0{-}_{ℝ}B$$
25	10	adantr	$$⊢\left(\phi \wedge 0<0{-}_{ℝ}AB\right)\to 1{/}_{ℝ}A\in ℝ$$
26		rernegcl	$$⊢AB\in ℝ\to 0{-}_{ℝ}AB\in ℝ$$
27	11 26	syl	$$⊢\phi \to 0{-}_{ℝ}AB\in ℝ$$
28	27	adantr	$$⊢\left(\phi \wedge 0<0{-}_{ℝ}AB\right)\to 0{-}_{ℝ}AB\in ℝ$$
29	1 3	sn-reclt0d	$$⊢\phi \to 1{/}_{ℝ}A<0$$
30	29	adantr	$$⊢\left(\phi \wedge 0<0{-}_{ℝ}AB\right)\to 1{/}_{ℝ}A<0$$
31		simpr	$$⊢\left(\phi \wedge 0<0{-}_{ℝ}AB\right)\to 0<0{-}_{ℝ}AB$$
32	25 28 30 31	mulltgt0d	$$⊢\left(\phi \wedge 0<0{-}_{ℝ}AB\right)\to \left(1{/}_{ℝ}A\right)\left(0{-}_{ℝ}AB\right)<0$$
33	24 32	eqbrtrrd	$$⊢\left(\phi \wedge 0<0{-}_{ℝ}AB\right)\to 0{-}_{ℝ}B<0$$
34	33	ex	$$⊢\phi \to \left(0<0{-}_{ℝ}AB\to 0{-}_{ℝ}B<0\right)$$
35		relt0neg1	$$⊢AB\in ℝ\to \left(AB<0\leftrightarrow 0<0{-}_{ℝ}AB\right)$$
36	11 35	syl	$$⊢\phi \to \left(AB<0\leftrightarrow 0<0{-}_{ℝ}AB\right)$$
37		relt0neg2	$$⊢B\in ℝ\to \left(0<B\leftrightarrow 0{-}_{ℝ}B<0\right)$$
38	2 37	syl	$$⊢\phi \to \left(0<B\leftrightarrow 0{-}_{ℝ}B<0\right)$$
39	34 36 38	3imtr4d	$$⊢\phi \to \left(AB<0\to 0<B\right)$$
40	39	imp	$$⊢\left(\phi \wedge AB<0\right)\to 0<B$$
41	8 40	impbida	$$⊢\phi \to \left(0<B\leftrightarrow AB<0\right)$$