Metamath Proof Explorer


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 )