Theorem mulgt0con1d

Description: Counterpart to mulgt0con2d , though not a lemma of anything. This is the first use of ax-pre-mulgt0 . (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 )