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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	mulgt0b2d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	mulgt0b2d.1	⊢ ( 𝜑 → 0 < 𝐴 )
Assertion	mulgt0b2d	⊢ ( 𝜑 → ( 0 < 𝐵 ↔ 0 < ( 𝐴 · 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulgt0b2d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		mulgt0b2d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		mulgt0b2d.1	⊢ ( 𝜑 → 0 < 𝐴 )
4	1	adantr	⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 𝐴 ∈ ℝ )
5	2	adantr	⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 𝐵 ∈ ℝ )
6	3	adantr	⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 0 < 𝐴 )
7		simpr	⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 0 < 𝐵 )
8	4 5 6 7	mulgt0d	⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 0 < ( 𝐴 · 𝐵 ) )
9	8	ex	⊢ ( 𝜑 → ( 0 < 𝐵 → 0 < ( 𝐴 · 𝐵 ) ) )
10	1	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ) → 𝐴 ∈ ℝ )
11		1re	⊢ 1 ∈ ℝ
12		rernegcl	⊢ ( 1 ∈ ℝ → ( 0 −ℝ 1 ) ∈ ℝ )
13	11 12	mp1i	⊢ ( 𝜑 → ( 0 −ℝ 1 ) ∈ ℝ )
14	2 13	remulcld	⊢ ( 𝜑 → ( 𝐵 · ( 0 −ℝ 1 ) ) ∈ ℝ )
15	14	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ) → ( 𝐵 · ( 0 −ℝ 1 ) ) ∈ ℝ )
16	3	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ) → 0 < 𝐴 )
17	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
18	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
19	13	recnd	⊢ ( 𝜑 → ( 0 −ℝ 1 ) ∈ ℂ )
20	17 18 19	mulassd	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) = ( 𝐴 · ( 𝐵 · ( 0 −ℝ 1 ) ) ) )
21	20	breq1d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ↔ ( 𝐴 · ( 𝐵 · ( 0 −ℝ 1 ) ) ) < 0 ) )
22	21	biimpa	⊢ ( ( 𝜑 ∧ ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ) → ( 𝐴 · ( 𝐵 · ( 0 −ℝ 1 ) ) ) < 0 )
23	10 15 16 22	mulgt0con2d	⊢ ( ( 𝜑 ∧ ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ) → ( 𝐵 · ( 0 −ℝ 1 ) ) < 0 )
24	23	ex	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 → ( 𝐵 · ( 0 −ℝ 1 ) ) < 0 ) )
25	1 2	remulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℝ )
26		relt0neg2	⊢ ( ( 𝐴 · 𝐵 ) ∈ ℝ → ( 0 < ( 𝐴 · 𝐵 ) ↔ ( 0 −ℝ ( 𝐴 · 𝐵 ) ) < 0 ) )
27	25 26	syl	⊢ ( 𝜑 → ( 0 < ( 𝐴 · 𝐵 ) ↔ ( 0 −ℝ ( 𝐴 · 𝐵 ) ) < 0 ) )
28		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
29	25 28	remulneg2d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) = ( 0 −ℝ ( ( 𝐴 · 𝐵 ) · 1 ) ) )
30		ax-1rid	⊢ ( ( 𝐴 · 𝐵 ) ∈ ℝ → ( ( 𝐴 · 𝐵 ) · 1 ) = ( 𝐴 · 𝐵 ) )
31	25 30	syl	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) · 1 ) = ( 𝐴 · 𝐵 ) )
32	31	oveq2d	⊢ ( 𝜑 → ( 0 −ℝ ( ( 𝐴 · 𝐵 ) · 1 ) ) = ( 0 −ℝ ( 𝐴 · 𝐵 ) ) )
33	29 32	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) = ( 0 −ℝ ( 𝐴 · 𝐵 ) ) )
34	33	breq1d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ↔ ( 0 −ℝ ( 𝐴 · 𝐵 ) ) < 0 ) )
35	27 34	bitr4d	⊢ ( 𝜑 → ( 0 < ( 𝐴 · 𝐵 ) ↔ ( ( 𝐴 · 𝐵 ) · ( 0 −ℝ 1 ) ) < 0 ) )
36		relt0neg2	⊢ ( 𝐵 ∈ ℝ → ( 0 < 𝐵 ↔ ( 0 −ℝ 𝐵 ) < 0 ) )
37	2 36	syl	⊢ ( 𝜑 → ( 0 < 𝐵 ↔ ( 0 −ℝ 𝐵 ) < 0 ) )
38	2 28	remulneg2d	⊢ ( 𝜑 → ( 𝐵 · ( 0 −ℝ 1 ) ) = ( 0 −ℝ ( 𝐵 · 1 ) ) )
39		ax-1rid	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 · 1 ) = 𝐵 )
40	2 39	syl	⊢ ( 𝜑 → ( 𝐵 · 1 ) = 𝐵 )
41	40	oveq2d	⊢ ( 𝜑 → ( 0 −ℝ ( 𝐵 · 1 ) ) = ( 0 −ℝ 𝐵 ) )
42	38 41	eqtrd	⊢ ( 𝜑 → ( 𝐵 · ( 0 −ℝ 1 ) ) = ( 0 −ℝ 𝐵 ) )
43	42	breq1d	⊢ ( 𝜑 → ( ( 𝐵 · ( 0 −ℝ 1 ) ) < 0 ↔ ( 0 −ℝ 𝐵 ) < 0 ) )
44	37 43	bitr4d	⊢ ( 𝜑 → ( 0 < 𝐵 ↔ ( 𝐵 · ( 0 −ℝ 1 ) ) < 0 ) )
45	24 35 44	3imtr4d	⊢ ( 𝜑 → ( 0 < ( 𝐴 · 𝐵 ) → 0 < 𝐵 ) )
46	9 45	impbid	⊢ ( 𝜑 → ( 0 < 𝐵 ↔ 0 < ( 𝐴 · 𝐵 ) ) )