mul2lt0bi

Description: If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018)

	Ref	Expression
Hypotheses	mul2lt0.1	$⊢ φ \to A \in ℝ$
	mul2lt0.2	$⊢ φ \to B \in ℝ$
Assertion	mul2lt0bi	$⊢ φ \to (A B < 0 \leftrightarrow ((A < 0 \land 0 < B) \lor (0 < A \land B < 0)))$

Proof

Step	Hyp	Ref	Expression
1		mul2lt0.1	$⊢ φ \to A \in ℝ$
2		mul2lt0.2	$⊢ φ \to B \in ℝ$
3	1 2	remulcld	$⊢ φ \to A B \in ℝ$
4		0red	$⊢ φ \to 0 \in ℝ$
5	3 4	ltnled	$⊢ φ \to (A B < 0 \leftrightarrow \neg 0 \leq A B)$
6	1	adantr	$⊢ (φ \land (0 \leq A \land 0 \leq B)) \to A \in ℝ$
7	2	adantr	$⊢ (φ \land (0 \leq A \land 0 \leq B)) \to B \in ℝ$
8		simprl	$⊢ (φ \land (0 \leq A \land 0 \leq B)) \to 0 \leq A$
9		simprr	$⊢ (φ \land (0 \leq A \land 0 \leq B)) \to 0 \leq B$
10	6 7 8 9	mulge0d	$⊢ (φ \land (0 \leq A \land 0 \leq B)) \to 0 \leq A B$
11	10	ex	$⊢ φ \to ((0 \leq A \land 0 \leq B) \to 0 \leq A B)$
12	11	con3d	$⊢ φ \to (\neg 0 \leq A B \to \neg (0 \leq A \land 0 \leq B))$
13	5 12	sylbid	$⊢ φ \to (A B < 0 \to \neg (0 \leq A \land 0 \leq B))$
14		ianor	$⊢ \neg (0 \leq A \land 0 \leq B) \leftrightarrow (\neg 0 \leq A \lor \neg 0 \leq B)$
15	13 14	syl6ib	$⊢ φ \to (A B < 0 \to (\neg 0 \leq A \lor \neg 0 \leq B))$
16	1 4	ltnled	$⊢ φ \to (A < 0 \leftrightarrow \neg 0 \leq A)$
17	2 4	ltnled	$⊢ φ \to (B < 0 \leftrightarrow \neg 0 \leq B)$
18	16 17	orbi12d	$⊢ φ \to ((A < 0 \lor B < 0) \leftrightarrow (\neg 0 \leq A \lor \neg 0 \leq B))$
19	15 18	sylibrd	$⊢ φ \to (A B < 0 \to (A < 0 \lor B < 0))$
20	19	imp	$⊢ (φ \land A B < 0) \to (A < 0 \lor B < 0)$
21		simpr	$⊢ ((φ \land A B < 0) \land A < 0) \to A < 0$
22	1	adantr	$⊢ (φ \land A B < 0) \to A \in ℝ$
23	2	adantr	$⊢ (φ \land A B < 0) \to B \in ℝ$
24		simpr	$⊢ (φ \land A B < 0) \to A B < 0$
25	22 23 24	mul2lt0llt0	$⊢ ((φ \land A B < 0) \land A < 0) \to 0 < B$
26	21 25	jca	$⊢ ((φ \land A B < 0) \land A < 0) \to (A < 0 \land 0 < B)$
27	26	ex	$⊢ (φ \land A B < 0) \to (A < 0 \to (A < 0 \land 0 < B))$
28	22 23 24	mul2lt0rlt0	$⊢ ((φ \land A B < 0) \land B < 0) \to 0 < A$
29		simpr	$⊢ ((φ \land A B < 0) \land B < 0) \to B < 0$
30	28 29	jca	$⊢ ((φ \land A B < 0) \land B < 0) \to (0 < A \land B < 0)$
31	30	ex	$⊢ (φ \land A B < 0) \to (B < 0 \to (0 < A \land B < 0))$
32	27 31	orim12d	$⊢ (φ \land A B < 0) \to ((A < 0 \lor B < 0) \to ((A < 0 \land 0 < B) \lor (0 < A \land B < 0)))$
33	20 32	mpd	$⊢ (φ \land A B < 0) \to ((A < 0 \land 0 < B) \lor (0 < A \land B < 0))$
34	1	adantr	$⊢ (φ \land (A < 0 \land 0 < B)) \to A \in ℝ$
35		0red	$⊢ (φ \land (A < 0 \land 0 < B)) \to 0 \in ℝ$
36	2	adantr	$⊢ (φ \land (A < 0 \land 0 < B)) \to B \in ℝ$
37		simprr	$⊢ (φ \land (A < 0 \land 0 < B)) \to 0 < B$
38	36 37	elrpd	$⊢ (φ \land (A < 0 \land 0 < B)) \to B \in ℝ^{+}$
39		simprl	$⊢ (φ \land (A < 0 \land 0 < B)) \to A < 0$
40	34 35 38 39	ltmul1dd	$⊢ (φ \land (A < 0 \land 0 < B)) \to A B < 0 \cdot B$
41	36	recnd	$⊢ (φ \land (A < 0 \land 0 < B)) \to B \in ℂ$
42	41	mul02d	$⊢ (φ \land (A < 0 \land 0 < B)) \to 0 \cdot B = 0$
43	40 42	breqtrd	$⊢ (φ \land (A < 0 \land 0 < B)) \to A B < 0$
44	2	adantr	$⊢ (φ \land (0 < A \land B < 0)) \to B \in ℝ$
45		0red	$⊢ (φ \land (0 < A \land B < 0)) \to 0 \in ℝ$
46	1	adantr	$⊢ (φ \land (0 < A \land B < 0)) \to A \in ℝ$
47		simprl	$⊢ (φ \land (0 < A \land B < 0)) \to 0 < A$
48	46 47	elrpd	$⊢ (φ \land (0 < A \land B < 0)) \to A \in ℝ^{+}$
49		simprr	$⊢ (φ \land (0 < A \land B < 0)) \to B < 0$
50	44 45 48 49	ltmul2dd	$⊢ (φ \land (0 < A \land B < 0)) \to A B < A \cdot 0$
51	46	recnd	$⊢ (φ \land (0 < A \land B < 0)) \to A \in ℂ$
52	51	mul01d	$⊢ (φ \land (0 < A \land B < 0)) \to A \cdot 0 = 0$
53	50 52	breqtrd	$⊢ (φ \land (0 < A \land B < 0)) \to A B < 0$
54	43 53	jaodan	$⊢ (φ \land ((A < 0 \land 0 < B) \lor (0 < A \land B < 0))) \to A B < 0$
55	33 54	impbida	$⊢ φ \to (A B < 0 \leftrightarrow ((A < 0 \land 0 < B) \lor (0 < A \land B < 0)))$

Metamath Proof Explorer

Theorem mul2lt0bi

Proof