This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )