mul2lt0rlt0

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 ℝ$
	mul2lt0.3	$⊢ φ \to A B < 0$
Assertion	mul2lt0rlt0	$⊢ (φ \land B < 0) \to 0 < A$

Proof

Step	Hyp	Ref	Expression
1		mul2lt0.1	$⊢ φ \to A \in ℝ$
2		mul2lt0.2	$⊢ φ \to B \in ℝ$
3		mul2lt0.3	$⊢ φ \to A B < 0$
4	1 2	remulcld	$⊢ φ \to A B \in ℝ$
5	4	adantr	$⊢ (φ \land B < 0) \to A B \in ℝ$
6		0red	$⊢ (φ \land B < 0) \to 0 \in ℝ$
7		negelrp	$⊢ B \in ℝ \to (- B \in ℝ^{+} \leftrightarrow B < 0)$
8	2 7	syl	$⊢ φ \to (- B \in ℝ^{+} \leftrightarrow B < 0)$
9	8	biimpar	$⊢ (φ \land B < 0) \to - B \in ℝ^{+}$
10	3	adantr	$⊢ (φ \land B < 0) \to A B < 0$
11	5 6 9 10	ltdiv1dd	$⊢ (φ \land B < 0) \to \frac{A B}{- B} < \frac{0}{- B}$
12	1	recnd	$⊢ φ \to A \in ℂ$
13	12	adantr	$⊢ (φ \land B < 0) \to A \in ℂ$
14	2	recnd	$⊢ φ \to B \in ℂ$
15	14	adantr	$⊢ (φ \land B < 0) \to B \in ℂ$
16	13 15	mulcld	$⊢ (φ \land B < 0) \to A B \in ℂ$
17		simpr	$⊢ (φ \land B < 0) \to B < 0$
18	17	lt0ne0d	$⊢ (φ \land B < 0) \to B \neq 0$
19	16 15 18	divneg2d	$⊢ (φ \land B < 0) \to - \frac{A B}{B} = \frac{A B}{- B}$
20	13 15 18	divcan4d	$⊢ (φ \land B < 0) \to \frac{A B}{B} = A$
21	20	negeqd	$⊢ (φ \land B < 0) \to - \frac{A B}{B} = - A$
22	19 21	eqtr3d	$⊢ (φ \land B < 0) \to \frac{A B}{- B} = - A$
23	15	negcld	$⊢ (φ \land B < 0) \to - B \in ℂ$
24	15 18	negne0d	$⊢ (φ \land B < 0) \to - B \neq 0$
25	23 24	div0d	$⊢ (φ \land B < 0) \to \frac{0}{- B} = 0$
26	11 22 25	3brtr3d	$⊢ (φ \land B < 0) \to - A < 0$
27	1	adantr	$⊢ (φ \land B < 0) \to A \in ℝ$
28	27	lt0neg2d	$⊢ (φ \land B < 0) \to (0 < A \leftrightarrow - A < 0)$
29	26 28	mpbird	$⊢ (φ \land B < 0) \to 0 < A$

Metamath Proof Explorer

Theorem mul2lt0rlt0

Proof