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	$⊢ φ \to A \in ℝ$
	mullt0b1d.b	$⊢ φ \to B \in ℝ$
	mullt0b1d.1	$⊢ φ \to A < 0$
Assertion	mullt0b1d	$⊢ φ \to (0 < B \leftrightarrow A B < 0)$

Proof

Step	Hyp	Ref	Expression
1		mullt0b1d.a	$⊢ φ \to A \in ℝ$
2		mullt0b1d.b	$⊢ φ \to B \in ℝ$
3		mullt0b1d.1	$⊢ φ \to A < 0$
4	1	adantr	$⊢ (φ \land 0 < B) \to A \in ℝ$
5	2	adantr	$⊢ (φ \land 0 < B) \to B \in ℝ$
6	3	adantr	$⊢ (φ \land 0 < B) \to A < 0$
7		simpr	$⊢ (φ \land 0 < B) \to 0 < B$
8	4 5 6 7	mulltgt0d	$⊢ (φ \land 0 < B) \to A B < 0$
9	3	lt0ne0d	$⊢ φ \to A \neq 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	$⊢ φ \to A B \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	rerecid2d	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	$⊢ φ \to A \in ℂ$
17	2	recnd	$⊢ φ \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 1 B = B$
20	2 19	syl	$⊢ φ \to 1 B = 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	$⊢ A B \in ℝ \to 0 -_{ℝ} A B \in ℝ$
27	11 26	syl	$⊢ φ \to 0 -_{ℝ} A B \in ℝ$
28	27	adantr	$⊢ (φ \land 0 < 0 -_{ℝ} A B) \to 0 -_{ℝ} A B \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	$⊢ (φ \land 0 < 0 -_{ℝ} A B) \to 0 < 0 -_{ℝ} A B$
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	$⊢ (φ \land 0 < 0 -_{ℝ} A B) \to 0 -_{ℝ} B < 0$
34	33	ex	$⊢ φ \to (0 < 0 -_{ℝ} A B \to 0 -_{ℝ} B < 0)$
35		relt0neg1	$⊢ A B \in ℝ \to (A B < 0 \leftrightarrow 0 < 0 -_{ℝ} A B)$
36	11 35	syl	$⊢ φ \to (A B < 0 \leftrightarrow 0 < 0 -_{ℝ} A B)$
37		relt0neg2	$⊢ B \in ℝ \to (0 < B \leftrightarrow 0 -_{ℝ} B < 0)$
38	2 37	syl	$⊢ φ \to (0 < B \leftrightarrow 0 -_{ℝ} B < 0)$
39	34 36 38	3imtr4d	$⊢ φ \to (A B < 0 \to 0 < B)$
40	39	imp	$⊢ (φ \land A B < 0) \to 0 < B$
41	8 40	impbida	$⊢ φ \to (0 < B \leftrightarrow A B < 0)$

Metamath Proof Explorer

Theorem mullt0b1d

Proof