Theorem mulgt0con2d

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

	Ref	Expression
Hypotheses	mulgt0con2d.a	$$⊢\phi \to A\in ℝ$$
	mulgt0con2d.b	$$⊢\phi \to B\in ℝ$$
	mulgt0con2d.1	$$⊢\phi \to 0<A$$
	mulgt0con2d.2	$$⊢\phi \to AB<0$$
Assertion	mulgt0con2d	$$⊢\phi \to B<0$$

Proof

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