Theorem mulltgt0

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

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

Proof

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