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

Proof

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