Theorem mullt0

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

	Ref	Expression
Assertion	mullt0	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 < 0 ) ) → 0 < ( 𝐴 · 𝐵 ) )

Proof

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