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	imbitrdi	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 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 ) ) ) )