Metamath Proof Explorer

Theorem mul2lt0bi

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

Proof

Step Hyp Ref Expression
1 mul2lt0.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 mul2lt0.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 1 2 remulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℝ )
4 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
5 3 4 ltnled ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 ↔ ¬ 0 ≤ ( 𝐴 · 𝐵 ) ) )
6 1 adantr ⊢ ( ( 𝜑 ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 𝐴 ∈ ℝ )
7 2 adantr ⊢ ( ( 𝜑 ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 𝐵 ∈ ℝ )
8 simprl ⊢ ( ( 𝜑 ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ≤ 𝐴 )
9 simprr ⊢ ( ( 𝜑 ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ≤ 𝐵 )
10 6 7 8 9 mulge0d ⊢ ( ( 𝜑 ∧ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 · 𝐵 ) )
11 10 ex ⊢ ( 𝜑 → ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → 0 ≤ ( 𝐴 · 𝐵 ) ) )
12 11 con3d ⊢ ( 𝜑 → ( ¬ 0 ≤ ( 𝐴 · 𝐵 ) → ¬ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) )
13 5 12 sylbid ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 → ¬ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ) )
14 ianor ⊢ ( ¬ ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) ↔ ( ¬ 0 ≤ 𝐴 ∨ ¬ 0 ≤ 𝐵 ) )
15 13 14 syl6ib ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 → ( ¬ 0 ≤ 𝐴 ∨ ¬ 0 ≤ 𝐵 ) ) )
16 1 4 ltnled ⊢ ( 𝜑 → ( 𝐴 < 0 ↔ ¬ 0 ≤ 𝐴 ) )
17 2 4 ltnled ⊢ ( 𝜑 → ( 𝐵 < 0 ↔ ¬ 0 ≤ 𝐵 ) )
18 16 17 orbi12d ⊢ ( 𝜑 → ( ( 𝐴 < 0 ∨ 𝐵 < 0 ) ↔ ( ¬ 0 ≤ 𝐴 ∨ ¬ 0 ≤ 𝐵 ) ) )
19 15 18 sylibrd ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 → ( 𝐴 < 0 ∨ 𝐵 < 0 ) ) )
20 19 imp ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 𝐴 < 0 ∨ 𝐵 < 0 ) )
21 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) ∧ 𝐴 < 0 ) → 𝐴 < 0 )
22 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → 𝐴 ∈ ℝ )
23 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → 𝐵 ∈ ℝ )
24 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 𝐴 · 𝐵 ) < 0 )
25 22 23 24 mul2lt0llt0 ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) ∧ 𝐴 < 0 ) → 0 < 𝐵 )
26 21 25 jca ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) ∧ 𝐴 < 0 ) → ( 𝐴 < 0 ∧ 0 < 𝐵 ) )
27 26 ex ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 𝐴 < 0 → ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) )
28 22 23 24 mul2lt0rlt0 ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) ∧ 𝐵 < 0 ) → 0 < 𝐴 )
29 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) ∧ 𝐵 < 0 ) → 𝐵 < 0 )
30 28 29 jca ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) ∧ 𝐵 < 0 ) → ( 0 < 𝐴 ∧ 𝐵 < 0 ) )
31 30 ex ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( 𝐵 < 0 → ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) )
32 27 31 orim12d ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( ( 𝐴 < 0 ∨ 𝐵 < 0 ) → ( ( 𝐴 < 0 ∧ 0 < 𝐵 ) ∨ ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) ) )
33 20 32 mpd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → ( ( 𝐴 < 0 ∧ 0 < 𝐵 ) ∨ ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) )
34 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) → 𝐴 ∈ ℝ )
35 0red ⊢ ( ( 𝜑 ∧ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) → 0 ∈ ℝ )
36 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) → 𝐵 ∈ ℝ )
37 simprr ⊢ ( ( 𝜑 ∧ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) → 0 < 𝐵 )
38 36 37 elrpd ⊢ ( ( 𝜑 ∧ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) → 𝐵 ∈ ℝ+ )
39 simprl ⊢ ( ( 𝜑 ∧ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) → 𝐴 < 0 )
40 34 35 38 39 ltmul1dd ⊢ ( ( 𝜑 ∧ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) → ( 𝐴 · 𝐵 ) < ( 0 · 𝐵 ) )
41 36 recnd ⊢ ( ( 𝜑 ∧ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) → 𝐵 ∈ ℂ )
42 41 mul02d ⊢ ( ( 𝜑 ∧ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) → ( 0 · 𝐵 ) = 0 )
43 40 42 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 < 0 ∧ 0 < 𝐵 ) ) → ( 𝐴 · 𝐵 ) < 0 )
44 2 adantr ⊢ ( ( 𝜑 ∧ ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) → 𝐵 ∈ ℝ )
45 0red ⊢ ( ( 𝜑 ∧ ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) → 0 ∈ ℝ )
46 1 adantr ⊢ ( ( 𝜑 ∧ ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) → 𝐴 ∈ ℝ )
47 simprl ⊢ ( ( 𝜑 ∧ ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) → 0 < 𝐴 )
48 46 47 elrpd ⊢ ( ( 𝜑 ∧ ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) → 𝐴 ∈ ℝ+ )
49 simprr ⊢ ( ( 𝜑 ∧ ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) → 𝐵 < 0 )
50 44 45 48 49 ltmul2dd ⊢ ( ( 𝜑 ∧ ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) → ( 𝐴 · 𝐵 ) < ( 𝐴 · 0 ) )
51 46 recnd ⊢ ( ( 𝜑 ∧ ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) → 𝐴 ∈ ℂ )
52 51 mul01d ⊢ ( ( 𝜑 ∧ ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) → ( 𝐴 · 0 ) = 0 )
53 50 52 breqtrd ⊢ ( ( 𝜑 ∧ ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) → ( 𝐴 · 𝐵 ) < 0 )
54 43 53 jaodan ⊢ ( ( 𝜑 ∧ ( ( 𝐴 < 0 ∧ 0 < 𝐵 ) ∨ ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) ) → ( 𝐴 · 𝐵 ) < 0 )
55 33 54 impbida ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 ↔ ( ( 𝐴 < 0 ∧ 0 < 𝐵 ) ∨ ( 0 < 𝐴 ∧ 𝐵 < 0 ) ) ) )