Metamath Proof Explorer

Theorem mul2lt0rlt0

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 ⊢ φ → A ∈ ℝ
mul2lt0.2 ⊢ φ → B ∈ ℝ
mul2lt0.3 ⊢ φ → A ⁢ B < 0
Assertion mul2lt0rlt0 ⊢ φ ∧ B < 0 → 0 < A

Proof

Step Hyp Ref Expression
1 mul2lt0.1 ⊢ φ → A ∈ ℝ
2 mul2lt0.2 ⊢ φ → B ∈ ℝ
3 mul2lt0.3 ⊢ φ → A ⁢ B < 0
4 1 2 remulcld ⊢ φ → A ⁢ B ∈ ℝ
5 4 adantr ⊢ φ ∧ B < 0 → A ⁢ B ∈ ℝ
6 0red ⊢ φ ∧ B < 0 → 0 ∈ ℝ
7 negelrp ⊢ B ∈ ℝ → − B ∈ ℝ + ↔ B < 0
8 2 7 syl ⊢ φ → − B ∈ ℝ + ↔ B < 0
9 8 biimpar ⊢ φ ∧ B < 0 → − B ∈ ℝ +
10 3 adantr ⊢ φ ∧ B < 0 → A ⁢ B < 0
11 5 6 9 10 ltdiv1dd ⊢ φ ∧ B < 0 → A ⁢ B − B < 0 − B
12 1 recnd ⊢ φ → A ∈ ℂ
13 12 adantr ⊢ φ ∧ B < 0 → A ∈ ℂ
14 2 recnd ⊢ φ → B ∈ ℂ
15 14 adantr ⊢ φ ∧ B < 0 → B ∈ ℂ
16 13 15 mulcld ⊢ φ ∧ B < 0 → A ⁢ B ∈ ℂ
17 simpr ⊢ φ ∧ B < 0 → B < 0
18 17 lt0ne0d ⊢ φ ∧ B < 0 → B ≠ 0
19 16 15 18 divneg2d ⊢ φ ∧ B < 0 → − A ⁢ B B = A ⁢ B − B
20 13 15 18 divcan4d ⊢ φ ∧ B < 0 → A ⁢ B B = A
21 20 negeqd ⊢ φ ∧ B < 0 → − A ⁢ B B = − A
22 19 21 eqtr3d ⊢ φ ∧ B < 0 → A ⁢ B − B = − A
23 15 negcld ⊢ φ ∧ B < 0 → − B ∈ ℂ
24 15 18 negne0d ⊢ φ ∧ B < 0 → − B ≠ 0
25 23 24 div0d ⊢ φ ∧ B < 0 → 0 − B = 0
26 11 22 25 3brtr3d ⊢ φ ∧ B < 0 → − A < 0
27 1 adantr ⊢ φ ∧ B < 0 → A ∈ ℝ
28 27 lt0neg2d ⊢ φ ∧ B < 0 → 0 < A ↔ − A < 0
29 26 28 mpbird ⊢ φ ∧ B < 0 → 0 < A