Theorem mulgt0b2d

Description: Biconditional, deductive form of mulgt0 . The second factor is positive iff the product is. Note that the commuted form cannot be proven since resubdi does not have a commuted form. (Contributed by SN, 26-Jun-2024)

	Ref	Expression
Hypotheses	mulgt0b2d.a	$$⊢\phi \to A\in ℝ$$
	mulgt0b2d.b	$$⊢\phi \to B\in ℝ$$
	mulgt0b2d.1	$$⊢\phi \to 0<A$$
Assertion	mulgt0b2d	$$⊢\phi \to \left(0<B\leftrightarrow 0<AB\right)$$

Proof

Step	Hyp	Ref	Expression
1		mulgt0b2d.a	$$⊢\phi \to A\in ℝ$$
2		mulgt0b2d.b	$$⊢\phi \to B\in ℝ$$
3		mulgt0b2d.1	$$⊢\phi \to 0<A$$
4	1	adantr	$$⊢\left(\phi \wedge 0<B\right)\to A\in ℝ$$
5	2	adantr	$$⊢\left(\phi \wedge 0<B\right)\to B\in ℝ$$
6	3	adantr	$$⊢\left(\phi \wedge 0<B\right)\to 0<A$$
7		simpr	$$⊢\left(\phi \wedge 0<B\right)\to 0<B$$
8	4 5 6 7	mulgt0d	$$⊢\left(\phi \wedge 0<B\right)\to 0<AB$$
9	8	ex	$$⊢\phi \to \left(0<B\to 0<AB\right)$$
10	1	adantr	$$⊢\left(\phi \wedge AB\left(0{-}_{ℝ}1\right)<0\right)\to A\in ℝ$$
11		1re	$$⊢1\in ℝ$$
12		rernegcl	$$⊢1\in ℝ\to 0{-}_{ℝ}1\in ℝ$$
13	11 12	mp1i	$$⊢\phi \to 0{-}_{ℝ}1\in ℝ$$
14	2 13	remulcld	$$⊢\phi \to B\left(0{-}_{ℝ}1\right)\in ℝ$$
15	14	adantr	$$⊢\left(\phi \wedge AB\left(0{-}_{ℝ}1\right)<0\right)\to B\left(0{-}_{ℝ}1\right)\in ℝ$$
16	3	adantr	$$⊢\left(\phi \wedge AB\left(0{-}_{ℝ}1\right)<0\right)\to 0<A$$
17	1	recnd	$$⊢\phi \to A\in ℂ$$
18	2	recnd	$$⊢\phi \to B\in ℂ$$
19	13	recnd	$$⊢\phi \to 0{-}_{ℝ}1\in ℂ$$
20	17 18 19	mulassd	$$⊢\phi \to AB\left(0{-}_{ℝ}1\right)=AB\left(0{-}_{ℝ}1\right)$$
21	20	breq1d	$$⊢\phi \to \left(AB\left(0{-}_{ℝ}1\right)<0\leftrightarrow AB\left(0{-}_{ℝ}1\right)<0\right)$$
22	21	biimpa	$$⊢\left(\phi \wedge AB\left(0{-}_{ℝ}1\right)<0\right)\to AB\left(0{-}_{ℝ}1\right)<0$$
23	10 15 16 22	mulgt0con2d	$$⊢\left(\phi \wedge AB\left(0{-}_{ℝ}1\right)<0\right)\to B\left(0{-}_{ℝ}1\right)<0$$
24	23	ex	$$⊢\phi \to \left(AB\left(0{-}_{ℝ}1\right)<0\to B\left(0{-}_{ℝ}1\right)<0\right)$$
25	1 2	remulcld	$$⊢\phi \to AB\in ℝ$$
26		relt0neg2	$$⊢AB\in ℝ\to \left(0<AB\leftrightarrow 0{-}_{ℝ}AB<0\right)$$
27	25 26	syl	$$⊢\phi \to \left(0<AB\leftrightarrow 0{-}_{ℝ}AB<0\right)$$
28		1red	$$⊢\phi \to 1\in ℝ$$
29	25 28	remulneg2d	$$⊢\phi \to AB\left(0{-}_{ℝ}1\right)=0{-}_{ℝ}AB\cdot 1$$
30		ax-1rid	$$⊢AB\in ℝ\to AB\cdot 1=AB$$
31	25 30	syl	$$⊢\phi \to AB\cdot 1=AB$$
32	31	oveq2d	$$⊢\phi \to 0{-}_{ℝ}AB\cdot 1=0{-}_{ℝ}AB$$
33	29 32	eqtrd	$$⊢\phi \to AB\left(0{-}_{ℝ}1\right)=0{-}_{ℝ}AB$$
34	33	breq1d	$$⊢\phi \to \left(AB\left(0{-}_{ℝ}1\right)<0\leftrightarrow 0{-}_{ℝ}AB<0\right)$$
35	27 34	bitr4d	$$⊢\phi \to \left(0<AB\leftrightarrow AB\left(0{-}_{ℝ}1\right)<0\right)$$
36		relt0neg2	$$⊢B\in ℝ\to \left(0<B\leftrightarrow 0{-}_{ℝ}B<0\right)$$
37	2 36	syl	$$⊢\phi \to \left(0<B\leftrightarrow 0{-}_{ℝ}B<0\right)$$
38	2 28	remulneg2d	$$⊢\phi \to B\left(0{-}_{ℝ}1\right)=0{-}_{ℝ}B\cdot 1$$
39		ax-1rid	$$⊢B\in ℝ\to B\cdot 1=B$$
40	2 39	syl	$$⊢\phi \to B\cdot 1=B$$
41	40	oveq2d	$$⊢\phi \to 0{-}_{ℝ}B\cdot 1=0{-}_{ℝ}B$$
42	38 41	eqtrd	$$⊢\phi \to B\left(0{-}_{ℝ}1\right)=0{-}_{ℝ}B$$
43	42	breq1d	$$⊢\phi \to \left(B\left(0{-}_{ℝ}1\right)<0\leftrightarrow 0{-}_{ℝ}B<0\right)$$
44	37 43	bitr4d	$$⊢\phi \to \left(0<B\leftrightarrow B\left(0{-}_{ℝ}1\right)<0\right)$$
45	24 35 44	3imtr4d	$$⊢\phi \to \left(0<AB\to 0<B\right)$$
46	9 45	impbid	$$⊢\phi \to \left(0<B\leftrightarrow 0<AB\right)$$