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