Metamath Proof Explorer

Theorem mul2lt0rgt0

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	mul2lt0rgt0	$⊢ (φ \land 0 < B) \to A < 0$

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	3	adantr	$⊢ (φ \land 0 < B) \to A B < 0$
5	2	adantr	$⊢ (φ \land 0 < B) \to B \in ℝ$
6	5	recnd	$⊢ (φ \land 0 < B) \to B \in ℂ$
7	6	mul02d	$⊢ (φ \land 0 < B) \to 0 \cdot B = 0$
8	4 7	breqtrrd	$⊢ (φ \land 0 < B) \to A B < 0 \cdot B$
9	1	adantr	$⊢ (φ \land 0 < B) \to A \in ℝ$
10		0red	$⊢ (φ \land 0 < B) \to 0 \in ℝ$
11		simpr	$⊢ (φ \land 0 < B) \to 0 < B$
12	5 11	elrpd	$⊢ (φ \land 0 < B) \to B \in ℝ^{+}$
13	9 10 12	ltmul1d	$⊢ (φ \land 0 < B) \to (A < 0 \leftrightarrow A B < 0 \cdot B)$
14	8 13	mpbird	$⊢ (φ \land 0 < B) \to A < 0$