mullt0

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

		Ref	Expression
	Assertion	mullt0	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land B < 0)) \to 0 < A B$

Step	Hyp	Ref	Expression
1		renegcl	$⊢ A \in ℝ \to - A \in ℝ$
2	1	adantr	$⊢ (A \in ℝ \land A < 0) \to - A \in ℝ$
3		lt0neg1	$⊢ A \in ℝ \to (A < 0 \leftrightarrow 0 < - A)$
4	3	biimpa	$⊢ (A \in ℝ \land A < 0) \to 0 < - A$
5	2 4	jca	$⊢ (A \in ℝ \land A < 0) \to (- A \in ℝ \land 0 < - A)$
6		renegcl	$⊢ B \in ℝ \to - B \in ℝ$
7	6	adantr	$⊢ (B \in ℝ \land B < 0) \to - B \in ℝ$
8		lt0neg1	$⊢ B \in ℝ \to (B < 0 \leftrightarrow 0 < - B)$
9	8	biimpa	$⊢ (B \in ℝ \land B < 0) \to 0 < - B$
10	7 9	jca	$⊢ (B \in ℝ \land B < 0) \to (- B \in ℝ \land 0 < - B)$
11		mulgt0	$⊢ ((- A \in ℝ \land 0 < - A) \land (- B \in ℝ \land 0 < - B)) \to 0 < (- A) (- B)$
12	5 10 11	syl2an	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land B < 0)) \to 0 < (- A) (- B)$
13		recn	$⊢ A \in ℝ \to A \in ℂ$
14		recn	$⊢ B \in ℝ \to B \in ℂ$
15		mul2neg	$⊢ (A \in ℂ \land B \in ℂ) \to (- A) (- B) = A B$
16	13 14 15	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to (- A) (- B) = A B$
17	16	ad2ant2r	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land B < 0)) \to (- A) (- B) = A B$
18	12 17	breqtrd	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land B < 0)) \to 0 < A B$

Metamath Proof Explorer