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

Metamath Proof Explorer

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 < ( 𝐴 · 𝐵 ) )