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	Could not format ( ( ph /\ 0 < ( A x. B ) ) -> ( 1 /R B ) e. RR ) : No typesetting found for |- ( ( ph /\ 0 < ( A x. B ) ) -> ( 1 /R B ) e. RR ) with typecode |-
21	2 3	sn-recgt0d	Could not format ( ph -> 0 < ( 1 /R B ) ) : No typesetting found for |- ( ph -> 0 < ( 1 /R B ) ) with typecode |-
22	21	adantr	Could not format ( ( ph /\ 0 < ( A x. B ) ) -> 0 < ( 1 /R B ) ) : No typesetting found for |- ( ( ph /\ 0 < ( A x. B ) ) -> 0 < ( 1 /R B ) ) with typecode |-
23	10 20 12 22	mulgt0d	Could not format ( ( ph /\ 0 < ( A x. B ) ) -> 0 < ( ( A x. B ) x. ( 1 /R B ) ) ) : No typesetting found for |- ( ( ph /\ 0 < ( A x. B ) ) -> 0 < ( ( A x. B ) x. ( 1 /R B ) ) ) with typecode |-
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	Could not format ( ( ph /\ 0 < ( A x. B ) ) -> ( 1 /R B ) e. CC ) : No typesetting found for |- ( ( ph /\ 0 < ( A x. B ) ) -> ( 1 /R B ) e. CC ) with typecode |-
27	24 25 26	mulassd	Could not format ( ( ph /\ 0 < ( A x. B ) ) -> ( ( A x. B ) x. ( 1 /R B ) ) = ( A x. ( B x. ( 1 /R B ) ) ) ) : No typesetting found for |- ( ( ph /\ 0 < ( A x. B ) ) -> ( ( A x. B ) x. ( 1 /R B ) ) = ( A x. ( B x. ( 1 /R B ) ) ) ) with typecode |-
28	3	gt0ne0d	$$⊢\phi \to B\ne 0$$
29	2 28	rerecid	Could not format ( ph -> ( B x. ( 1 /R B ) ) = 1 ) : No typesetting found for |- ( ph -> ( B x. ( 1 /R B ) ) = 1 ) with typecode |-
30	29	oveq2d	Could not format ( ph -> ( A x. ( B x. ( 1 /R B ) ) ) = ( A x. 1 ) ) : No typesetting found for |- ( ph -> ( A x. ( B x. ( 1 /R B ) ) ) = ( A x. 1 ) ) with typecode |-
31	30	adantr	Could not format ( ( ph /\ 0 < ( A x. B ) ) -> ( A x. ( B x. ( 1 /R B ) ) ) = ( A x. 1 ) ) : No typesetting found for |- ( ( ph /\ 0 < ( A x. B ) ) -> ( A x. ( B x. ( 1 /R B ) ) ) = ( A x. 1 ) ) with typecode |-
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	Could not format ( ( ph /\ 0 < ( A x. B ) ) -> ( ( A x. B ) x. ( 1 /R B ) ) = A ) : No typesetting found for |- ( ( ph /\ 0 < ( A x. B ) ) -> ( ( A x. B ) x. ( 1 /R B ) ) = A ) with typecode |-
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)$$