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		0red	$$⊢\phi \to 0\in ℝ$$
29		1red	$$⊢\phi \to 1\in ℝ$$
30		resubdi	$$⊢\left(AB\in ℝ\wedge 0\in ℝ\wedge 1\in ℝ\right)\to AB\left(0{-}_{ℝ}1\right)=AB\cdot 0{-}_{ℝ}AB\cdot 1$$
31	25 28 29 30	syl3anc	$$⊢\phi \to AB\left(0{-}_{ℝ}1\right)=AB\cdot 0{-}_{ℝ}AB\cdot 1$$
32		remul01	$$⊢AB\in ℝ\to AB\cdot 0=0$$
33		ax-1rid	$$⊢AB\in ℝ\to AB\cdot 1=AB$$
34	32 33	oveq12d	$$⊢AB\in ℝ\to AB\cdot 0{-}_{ℝ}AB\cdot 1=0{-}_{ℝ}AB$$
35	25 34	syl	$$⊢\phi \to AB\cdot 0{-}_{ℝ}AB\cdot 1=0{-}_{ℝ}AB$$
36	31 35	eqtrd	$$⊢\phi \to AB\left(0{-}_{ℝ}1\right)=0{-}_{ℝ}AB$$
37	36	breq1d	$$⊢\phi \to \left(AB\left(0{-}_{ℝ}1\right)<0\leftrightarrow 0{-}_{ℝ}AB<0\right)$$
38	27 37	bitr4d	$$⊢\phi \to \left(0<AB\leftrightarrow AB\left(0{-}_{ℝ}1\right)<0\right)$$
39		relt0neg2	$$⊢B\in ℝ\to \left(0<B\leftrightarrow 0{-}_{ℝ}B<0\right)$$
40	2 39	syl	$$⊢\phi \to \left(0<B\leftrightarrow 0{-}_{ℝ}B<0\right)$$
41		resubdi	$$⊢\left(B\in ℝ\wedge 0\in ℝ\wedge 1\in ℝ\right)\to B\left(0{-}_{ℝ}1\right)=B\cdot 0{-}_{ℝ}B\cdot 1$$
42	2 28 29 41	syl3anc	$$⊢\phi \to B\left(0{-}_{ℝ}1\right)=B\cdot 0{-}_{ℝ}B\cdot 1$$
43		remul01	$$⊢B\in ℝ\to B\cdot 0=0$$
44		ax-1rid	$$⊢B\in ℝ\to B\cdot 1=B$$
45	43 44	oveq12d	$$⊢B\in ℝ\to B\cdot 0{-}_{ℝ}B\cdot 1=0{-}_{ℝ}B$$
46	2 45	syl	$$⊢\phi \to B\cdot 0{-}_{ℝ}B\cdot 1=0{-}_{ℝ}B$$
47	42 46	eqtrd	$$⊢\phi \to B\left(0{-}_{ℝ}1\right)=0{-}_{ℝ}B$$
48	47	breq1d	$$⊢\phi \to \left(B\left(0{-}_{ℝ}1\right)<0\leftrightarrow 0{-}_{ℝ}B<0\right)$$
49	40 48	bitr4d	$$⊢\phi \to \left(0<B\leftrightarrow B\left(0{-}_{ℝ}1\right)<0\right)$$
50	24 38 49	3imtr4d	$$⊢\phi \to \left(0<AB\to 0<B\right)$$
51	9 50	impbid	$$⊢\phi \to \left(0<B\leftrightarrow 0<AB\right)$$