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	$$⊢\phi \to A\in ℝ$$
	mulgt0con1d.b	$$⊢\phi \to B\in ℝ$$
	mulgt0con1d.1	$$⊢\phi \to 0<B$$
	mulgt0con1d.2	$$⊢\phi \to AB<0$$
Assertion	mulgt0con1d	$$⊢\phi \to A<0$$

Proof

Step	Hyp	Ref	Expression
1		mulgt0con1d.a	$$⊢\phi \to A\in ℝ$$
2		mulgt0con1d.b	$$⊢\phi \to B\in ℝ$$
3		mulgt0con1d.1	$$⊢\phi \to 0<B$$
4		mulgt0con1d.2	$$⊢\phi \to AB<0$$
5	1 2	remulcld	$$⊢\phi \to AB\in ℝ$$
6	1	adantr	$$⊢\left(\phi \wedge 0<A\right)\to A\in ℝ$$
7	2	adantr	$$⊢\left(\phi \wedge 0<A\right)\to B\in ℝ$$
8		simpr	$$⊢\left(\phi \wedge 0<A\right)\to 0<A$$
9	3	adantr	$$⊢\left(\phi \wedge 0<A\right)\to 0<B$$
10	6 7 8 9	mulgt0d	$$⊢\left(\phi \wedge 0<A\right)\to 0<AB$$
11	10	ex	$$⊢\phi \to \left(0<A\to 0<AB\right)$$
12		remul02	$$⊢B\in ℝ\to 0\cdot B=0$$
13	2 12	syl	$$⊢\phi \to 0\cdot B=0$$
14		oveq1	$$⊢A=0\to AB=0\cdot B$$
15	14	eqeq1d	$$⊢A=0\to \left(AB=0\leftrightarrow 0\cdot B=0\right)$$
16	13 15	syl5ibrcom	$$⊢\phi \to \left(A=0\to AB=0\right)$$
17	1 5 11 16	mulgt0con1dlem	$$⊢\phi \to \left(AB<0\to A<0\right)$$
18	4 17	mpd	$$⊢\phi \to A<0$$