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

Metamath Proof Explorer

Theorem mulgt0con1d

Description: Counterpart to mulgt0con2d , though not a lemma. This is the first use of ax-pre-mulgt0 . One direction of mulgt0b2d . (Contributed by SN, 26-Jun-2024)

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

Proof

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