Metamath Proof Explorer


Theorem mulgt0con2d

Description: Lemma for mulgt0b2d and contrapositive of mulgt0 . (Contributed by SN, 26-Jun-2024)

Ref Expression
Hypotheses mulgt0con2d.a ( 𝜑𝐴 ∈ ℝ )
mulgt0con2d.b ( 𝜑𝐵 ∈ ℝ )
mulgt0con2d.1 ( 𝜑 → 0 < 𝐴 )
mulgt0con2d.2 ( 𝜑 → ( 𝐴 · 𝐵 ) < 0 )
Assertion mulgt0con2d ( 𝜑𝐵 < 0 )

Proof

Step Hyp Ref Expression
1 mulgt0con2d.a ( 𝜑𝐴 ∈ ℝ )
2 mulgt0con2d.b ( 𝜑𝐵 ∈ ℝ )
3 mulgt0con2d.1 ( 𝜑 → 0 < 𝐴 )
4 mulgt0con2d.2 ( 𝜑 → ( 𝐴 · 𝐵 ) < 0 )
5 1 2 remulcld ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℝ )
6 1 adantr ( ( 𝜑 ∧ 0 < 𝐵 ) → 𝐴 ∈ ℝ )
7 2 adantr ( ( 𝜑 ∧ 0 < 𝐵 ) → 𝐵 ∈ ℝ )
8 3 adantr ( ( 𝜑 ∧ 0 < 𝐵 ) → 0 < 𝐴 )
9 simpr ( ( 𝜑 ∧ 0 < 𝐵 ) → 0 < 𝐵 )
10 6 7 8 9 mulgt0d ( ( 𝜑 ∧ 0 < 𝐵 ) → 0 < ( 𝐴 · 𝐵 ) )
11 10 ex ( 𝜑 → ( 0 < 𝐵 → 0 < ( 𝐴 · 𝐵 ) ) )
12 remul01 ( 𝐴 ∈ ℝ → ( 𝐴 · 0 ) = 0 )
13 1 12 syl ( 𝜑 → ( 𝐴 · 0 ) = 0 )
14 oveq2 ( 𝐵 = 0 → ( 𝐴 · 𝐵 ) = ( 𝐴 · 0 ) )
15 14 eqeq1d ( 𝐵 = 0 → ( ( 𝐴 · 𝐵 ) = 0 ↔ ( 𝐴 · 0 ) = 0 ) )
16 13 15 syl5ibrcom ( 𝜑 → ( 𝐵 = 0 → ( 𝐴 · 𝐵 ) = 0 ) )
17 2 5 11 16 mulgt0con1dlem ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 → 𝐵 < 0 ) )
18 4 17 mpd ( 𝜑𝐵 < 0 )