mulltgt0

Description: The product of a negative and a positive number is negative. (Contributed by Glauco Siliprandi, 20-Apr-2017)

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

Step	Hyp	Ref	Expression
1		renegcl	$⊢ A \in ℝ \to - A \in ℝ$
2	1	ad2antrr	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land 0 < B)) \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	4	adantr	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land 0 < B)) \to 0 < - A$
6		simpr	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land 0 < B)) \to (B \in ℝ \land 0 < B)$
7		mulgt0	$⊢ ((- A \in ℝ \land 0 < - A) \land (B \in ℝ \land 0 < B)) \to 0 < (- A) B$
8	2 5 6 7	syl21anc	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land 0 < B)) \to 0 < (- A) B$
9		recn	$⊢ A \in ℝ \to A \in ℂ$
10	9	ad2antrr	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land 0 < B)) \to A \in ℂ$
11		recn	$⊢ B \in ℝ \to B \in ℂ$
12	11	ad2antrl	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land 0 < B)) \to B \in ℂ$
13	10 12	mulneg1d	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land 0 < B)) \to (- A) B = - A B$
14	8 13	breqtrd	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land 0 < B)) \to 0 < - A B$
15		remulcl	$⊢ (A \in ℝ \land B \in ℝ) \to A B \in ℝ$
16	15	ad2ant2r	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land 0 < B)) \to A B \in ℝ$
17	16	lt0neg1d	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land 0 < B)) \to (A B < 0 \leftrightarrow 0 < - A B)$
18	14 17	mpbird	$⊢ ((A \in ℝ \land A < 0) \land (B \in ℝ \land 0 < B)) \to A B < 0$

Metamath Proof Explorer