This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )