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 ⊢ A ∈ ℝ ∧ A < 0 ∧ B ∈ ℝ ∧ 0 < B → A ⁢ B < 0

Proof

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