Theorem mulgt0b2d

Description: Biconditional, deductive form of mulgt0 . The first factor is positive iff the product is. (Contributed by SN, 24-Nov-2025)

	Ref	Expression
Hypotheses	mulgt0b2d.a	$$⊢\phi \to A\in ℝ$$
	mulgt0b2d.b	$$⊢\phi \to B\in ℝ$$
	mulgt0b2d.1	$$⊢\phi \to 0<B$$
Assertion	mulgt0b2d	$$⊢\phi \to \left(0<A\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<B$$
4	1	adantr	$$⊢\left(\phi \wedge 0<A\right)\to A\in ℝ$$
5	2	adantr	$$⊢\left(\phi \wedge 0<A\right)\to B\in ℝ$$
6		simpr	$$⊢\left(\phi \wedge 0<A\right)\to 0<A$$
7	3	adantr	$$⊢\left(\phi \wedge 0<A\right)\to 0<B$$
8	4 5 6 7	mulgt0d	$$⊢\left(\phi \wedge 0<A\right)\to 0<AB$$
9	1 2	remulcld	$$⊢\phi \to AB\in ℝ$$
10	9	adantr	$$⊢\left(\phi \wedge 0<AB\right)\to AB\in ℝ$$
11	2	adantr	$$⊢\left(\phi \wedge 0<AB\right)\to B\in ℝ$$
12		simpr	$$⊢\left(\phi \wedge 0<AB\right)\to 0<AB$$
13	12	gt0ne0d	$$⊢\left(\phi \wedge 0<AB\right)\to AB\ne 0$$
14		oveq2	$$⊢B=0\to AB=A\cdot 0$$
15	1	adantr	$$⊢\left(\phi \wedge 0<AB\right)\to A\in ℝ$$
16		remul01	$$⊢A\in ℝ\to A\cdot 0=0$$
17	15 16	syl	$$⊢\left(\phi \wedge 0<AB\right)\to A\cdot 0=0$$
18	14 17	sylan9eqr	$$⊢\left(\left(\phi \wedge 0<AB\right)\wedge B=0\right)\to AB=0$$
19	13 18	mteqand	$$⊢\left(\phi \wedge 0<AB\right)\to B\ne 0$$
20	11 19	sn-rereccld	$$⊢\left(\phi \wedge 0<AB\right)\to 1{/}_{ℝ}B\in ℝ$$
21	2 3	sn-recgt0d	$$⊢\phi \to 0<1{/}_{ℝ}B$$
22	21	adantr	$$⊢\left(\phi \wedge 0<AB\right)\to 0<1{/}_{ℝ}B$$
23	10 20 12 22	mulgt0d	$$⊢\left(\phi \wedge 0<AB\right)\to 0<AB\left(1{/}_{ℝ}B\right)$$
24	15	recnd	$$⊢\left(\phi \wedge 0<AB\right)\to A\in ℂ$$
25	11	recnd	$$⊢\left(\phi \wedge 0<AB\right)\to B\in ℂ$$
26	20	recnd	$$⊢\left(\phi \wedge 0<AB\right)\to 1{/}_{ℝ}B\in ℂ$$
27	24 25 26	mulassd	$$⊢\left(\phi \wedge 0<AB\right)\to AB\left(1{/}_{ℝ}B\right)=AB\left(1{/}_{ℝ}B\right)$$
28	3	gt0ne0d	$$⊢\phi \to B\ne 0$$
29	2 28	rerecidd	$$⊢\phi \to B\left(1{/}_{ℝ}B\right)=1$$
30	29	oveq2d	$$⊢\phi \to AB\left(1{/}_{ℝ}B\right)=A\cdot 1$$
31	30	adantr	$$⊢\left(\phi \wedge 0<AB\right)\to AB\left(1{/}_{ℝ}B\right)=A\cdot 1$$
32		ax-1rid	$$⊢A\in ℝ\to A\cdot 1=A$$
33	15 32	syl	$$⊢\left(\phi \wedge 0<AB\right)\to A\cdot 1=A$$
34	27 31 33	3eqtrd	$$⊢\left(\phi \wedge 0<AB\right)\to AB\left(1{/}_{ℝ}B\right)=A$$
35	23 34	breqtrd	$$⊢\left(\phi \wedge 0<AB\right)\to 0<A$$
36	8 35	impbida	$$⊢\phi \to \left(0<A\leftrightarrow 0<AB\right)$$