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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	mul2lt0.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	mul2lt0.3	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) < 0 )
Assertion	mul2lt0lgt0	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐵 < 0 )

Proof

Step	Hyp	Ref	Expression
1		mul2lt0.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		mul2lt0.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		mul2lt0.3	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) < 0 )
4	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
5	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
6	4 5	mulcomd	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
7	6 3	eqbrtrrd	⊢ ( 𝜑 → ( 𝐵 · 𝐴 ) < 0 )
8	2 1 7	mul2lt0rgt0	⊢ ( ( 𝜑 ∧ 0 < 𝐴 ) → 𝐵 < 0 )