Theorem mul2lt0lgt0

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

	Ref	Expression
Hypotheses	mul2lt0.1	$$⊢\phi \to A\in ℝ$$
	mul2lt0.2	$$⊢\phi \to B\in ℝ$$
	mul2lt0.3	$$⊢\phi \to AB<0$$
Assertion	mul2lt0lgt0	$$⊢\left(\phi \wedge 0<A\right)\to B<0$$

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	mul2lt0rgt0	$$⊢\left(\phi \wedge 0<A\right)\to B<0$$