Theorem mulle0b

Description: A condition for multiplication to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013)

	Ref	Expression
Assertion	mulle0b	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) ≤ 0 ↔ ( ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐵 ) ∨ ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 0 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		remulcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 · 𝐵 ) ∈ ℝ )
2	1	le0neg1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) ≤ 0 ↔ 0 ≤ - ( 𝐴 · 𝐵 ) ) )
3		le0neg2	⊢ ( 𝐵 ∈ ℝ → ( 0 ≤ 𝐵 ↔ - 𝐵 ≤ 0 ) )
4	3	anbi2d	⊢ ( 𝐵 ∈ ℝ → ( ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐵 ) ↔ ( 𝐴 ≤ 0 ∧ - 𝐵 ≤ 0 ) ) )
5		le0neg1	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 ≤ 0 ↔ 0 ≤ - 𝐵 ) )
6	5	anbi2d	⊢ ( 𝐵 ∈ ℝ → ( ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 0 ) ↔ ( 0 ≤ 𝐴 ∧ 0 ≤ - 𝐵 ) ) )
7	4 6	orbi12d	⊢ ( 𝐵 ∈ ℝ → ( ( ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐵 ) ∨ ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 0 ) ) ↔ ( ( 𝐴 ≤ 0 ∧ - 𝐵 ≤ 0 ) ∨ ( 0 ≤ 𝐴 ∧ 0 ≤ - 𝐵 ) ) ) )
8	7	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐵 ) ∨ ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 0 ) ) ↔ ( ( 𝐴 ≤ 0 ∧ - 𝐵 ≤ 0 ) ∨ ( 0 ≤ 𝐴 ∧ 0 ≤ - 𝐵 ) ) ) )
9		renegcl	⊢ ( 𝐵 ∈ ℝ → - 𝐵 ∈ ℝ )
10		mulge0b	⊢ ( ( 𝐴 ∈ ℝ ∧ - 𝐵 ∈ ℝ ) → ( 0 ≤ ( 𝐴 · - 𝐵 ) ↔ ( ( 𝐴 ≤ 0 ∧ - 𝐵 ≤ 0 ) ∨ ( 0 ≤ 𝐴 ∧ 0 ≤ - 𝐵 ) ) ) )
11	9 10	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ ( 𝐴 · - 𝐵 ) ↔ ( ( 𝐴 ≤ 0 ∧ - 𝐵 ≤ 0 ) ∨ ( 0 ≤ 𝐴 ∧ 0 ≤ - 𝐵 ) ) ) )
12		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
13		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
14		mulneg2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · - 𝐵 ) = - ( 𝐴 · 𝐵 ) )
15	14	breq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 0 ≤ ( 𝐴 · - 𝐵 ) ↔ 0 ≤ - ( 𝐴 · 𝐵 ) ) )
16	12 13 15	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ ( 𝐴 · - 𝐵 ) ↔ 0 ≤ - ( 𝐴 · 𝐵 ) ) )
17	8 11 16	3bitr2rd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ - ( 𝐴 · 𝐵 ) ↔ ( ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐵 ) ∨ ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 0 ) ) ) )
18	2 17	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) ≤ 0 ↔ ( ( 𝐴 ≤ 0 ∧ 0 ≤ 𝐵 ) ∨ ( 0 ≤ 𝐴 ∧ 𝐵 ≤ 0 ) ) ) )