Theorem mul2lt0llt0

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	$$⊢\phi \to A\in ℝ$$
	mul2lt0.2	$$⊢\phi \to B\in ℝ$$
	mul2lt0.3	$$⊢\phi \to AB<0$$
Assertion	mul2lt0llt0	$$⊢\left(\phi \wedge A<0\right)\to 0<B$$

Proof

Step	Hyp	Ref	Expression
1		mul2lt0.1	$$⊢\phi \to A\in ℝ$$
2		mul2lt0.2	$$⊢\phi \to B\in ℝ$$
3		mul2lt0.3	$$⊢\phi \to AB<0$$
4	1	recnd	$$⊢\phi \to A\in ℂ$$
5	2	recnd	$$⊢\phi \to B\in ℂ$$
6	4 5	mulcomd	$$⊢\phi \to AB=BA$$
7	6 3	eqbrtrrd	$$⊢\phi \to BA<0$$
8	2 1 7	mul2lt0rlt0	$$⊢\left(\phi \wedge A<0\right)\to 0<B$$