Metamath Proof Explorer

Theorem mulle0b

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

Ref Expression
Assertion mulle0b ⊢A∈ℝ∧B∈ℝ→A⁢B≤0↔A≤0∧0≤B∨0≤A∧B≤0

Proof

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