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	Could not format ( ph -> ( 1 /R A ) e. RR ) : No typesetting found for |- ( ph -> ( 1 /R A ) e. RR ) with typecode |-
11	1 2	remulcld	$$⊢\phi \to AB\in ℝ$$
12	10 11	remulneg2d	Could not format ( ph -> ( ( 1 /R A ) x. ( 0 -R ( A x. B ) ) ) = ( 0 -R ( ( 1 /R A ) x. ( A x. B ) ) ) ) : No typesetting found for |- ( ph -> ( ( 1 /R A ) x. ( 0 -R ( A x. B ) ) ) = ( 0 -R ( ( 1 /R A ) x. ( A x. B ) ) ) ) with typecode |-
13	1 9	rerecid2	Could not format ( ph -> ( ( 1 /R A ) x. A ) = 1 ) : No typesetting found for |- ( ph -> ( ( 1 /R A ) x. A ) = 1 ) with typecode |-
14	13	oveq1d	Could not format ( ph -> ( ( ( 1 /R A ) x. A ) x. B ) = ( 1 x. B ) ) : No typesetting found for |- ( ph -> ( ( ( 1 /R A ) x. A ) x. B ) = ( 1 x. B ) ) with typecode |-
15	10	recnd	Could not format ( ph -> ( 1 /R A ) e. CC ) : No typesetting found for |- ( ph -> ( 1 /R A ) e. CC ) with typecode |-
16	1	recnd	$$⊢\phi \to A\in ℂ$$
17	2	recnd	$$⊢\phi \to B\in ℂ$$
18	15 16 17	mulassd	Could not format ( ph -> ( ( ( 1 /R A ) x. A ) x. B ) = ( ( 1 /R A ) x. ( A x. B ) ) ) : No typesetting found for |- ( ph -> ( ( ( 1 /R A ) x. A ) x. B ) = ( ( 1 /R A ) x. ( A x. B ) ) ) with typecode |-
19		remullid	$$⊢B\in ℝ\to 1B=B$$
20	2 19	syl	$$⊢\phi \to 1B=B$$
21	14 18 20	3eqtr3d	Could not format ( ph -> ( ( 1 /R A ) x. ( A x. B ) ) = B ) : No typesetting found for |- ( ph -> ( ( 1 /R A ) x. ( A x. B ) ) = B ) with typecode |-
22	21	oveq2d	Could not format ( ph -> ( 0 -R ( ( 1 /R A ) x. ( A x. B ) ) ) = ( 0 -R B ) ) : No typesetting found for |- ( ph -> ( 0 -R ( ( 1 /R A ) x. ( A x. B ) ) ) = ( 0 -R B ) ) with typecode |-
23	12 22	eqtrd	Could not format ( ph -> ( ( 1 /R A ) x. ( 0 -R ( A x. B ) ) ) = ( 0 -R B ) ) : No typesetting found for |- ( ph -> ( ( 1 /R A ) x. ( 0 -R ( A x. B ) ) ) = ( 0 -R B ) ) with typecode |-
24	23	adantr	Could not format ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> ( ( 1 /R A ) x. ( 0 -R ( A x. B ) ) ) = ( 0 -R B ) ) : No typesetting found for |- ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> ( ( 1 /R A ) x. ( 0 -R ( A x. B ) ) ) = ( 0 -R B ) ) with typecode |-
25	10	adantr	Could not format ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> ( 1 /R A ) e. RR ) : No typesetting found for |- ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> ( 1 /R A ) e. RR ) with typecode |-
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	Could not format ( ph -> ( 1 /R A ) < 0 ) : No typesetting found for |- ( ph -> ( 1 /R A ) < 0 ) with typecode |-
30	29	adantr	Could not format ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> ( 1 /R A ) < 0 ) : No typesetting found for |- ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> ( 1 /R A ) < 0 ) with typecode |-
31		simpr	$$⊢\left(\phi \wedge 0<0{-}_{ℝ}AB\right)\to 0<0{-}_{ℝ}AB$$
32	25 28 30 31	mulltgt0d	Could not format ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> ( ( 1 /R A ) x. ( 0 -R ( A x. B ) ) ) < 0 ) : No typesetting found for |- ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> ( ( 1 /R A ) x. ( 0 -R ( A x. B ) ) ) < 0 ) with typecode |-
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)$$