Metamath Proof Explorer

Theorem mullt0

Description: The product of two negative numbers is positive. (Contributed by Jeff Hankins, 8-Jun-2009)

Ref Expression
Assertion mullt0 ⊢ A ∈ ℝ ∧ A < 0 ∧ B ∈ ℝ ∧ B < 0 → 0 < A ⁢ B

Proof

Step Hyp Ref Expression
1 renegcl ⊢ A ∈ ℝ → − A ∈ ℝ
2 1 adantr ⊢ A ∈ ℝ ∧ A < 0 → − A ∈ ℝ
3 lt0neg1 ⊢ A ∈ ℝ → A < 0 ↔ 0 < − A
4 3 biimpa ⊢ A ∈ ℝ ∧ A < 0 → 0 < − A
5 2 4 jca ⊢ A ∈ ℝ ∧ A < 0 → − A ∈ ℝ ∧ 0 < − A
6 renegcl ⊢ B ∈ ℝ → − B ∈ ℝ
7 6 adantr ⊢ B ∈ ℝ ∧ B < 0 → − B ∈ ℝ
8 lt0neg1 ⊢ B ∈ ℝ → B < 0 ↔ 0 < − B
9 8 biimpa ⊢ B ∈ ℝ ∧ B < 0 → 0 < − B
10 7 9 jca ⊢ B ∈ ℝ ∧ B < 0 → − B ∈ ℝ ∧ 0 < − B
11 mulgt0 ⊢ − A ∈ ℝ ∧ 0 < − A ∧ − B ∈ ℝ ∧ 0 < − B → 0 < − A ⁢ − B
12 5 10 11 syl2an ⊢ A ∈ ℝ ∧ A < 0 ∧ B ∈ ℝ ∧ B < 0 → 0 < − A ⁢ − B
13 recn ⊢ A ∈ ℝ → A ∈ ℂ
14 recn ⊢ B ∈ ℝ → B ∈ ℂ
15 mul2neg ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A ⁢ − B = A ⁢ B
16 13 14 15 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → − A ⁢ − B = A ⁢ B
17 16 ad2ant2r ⊢ A ∈ ℝ ∧ A < 0 ∧ B ∈ ℝ ∧ B < 0 → − A ⁢ − B = A ⁢ B
18 12 17 breqtrd ⊢ A ∈ ℝ ∧ A < 0 ∧ B ∈ ℝ ∧ B < 0 → 0 < A ⁢ B