Theorem lcmineqlem5

Description: Technical lemma for reciprocal multiplication in deduction form. (Contributed by metakunt, 10-May-2024)

	Ref	Expression
Hypotheses	lcmineqlem5.1	$$⊢\phi \to A\in ℂ$$
	lcmineqlem5.2	$$⊢\phi \to B\in ℂ$$
	lcmineqlem5.3	$$⊢\phi \to C\in ℂ$$
	lcmineqlem5.4	$$⊢\phi \to C\ne 0$$
Assertion	lcmineqlem5	$$⊢\phi \to AB\left(\frac{1}{C}\right)=B\left(\frac{A}{C}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem5.1	$$⊢\phi \to A\in ℂ$$
2		lcmineqlem5.2	$$⊢\phi \to B\in ℂ$$
3		lcmineqlem5.3	$$⊢\phi \to C\in ℂ$$
4		lcmineqlem5.4	$$⊢\phi \to C\ne 0$$
5	3 4	reccld	$$⊢\phi \to \frac{1}{C}\in ℂ$$
6	1 2 5	mulassd	$$⊢\phi \to AB\left(\frac{1}{C}\right)=AB\left(\frac{1}{C}\right)$$
7	1 2	mulcomd	$$⊢\phi \to AB=BA$$
8	7	oveq1d	$$⊢\phi \to AB\left(\frac{1}{C}\right)=BA\left(\frac{1}{C}\right)$$
9	6 8	eqtr3d	$$⊢\phi \to AB\left(\frac{1}{C}\right)=BA\left(\frac{1}{C}\right)$$
10	2 1 5	mulassd	$$⊢\phi \to BA\left(\frac{1}{C}\right)=BA\left(\frac{1}{C}\right)$$
11	9 10	eqtrd	$$⊢\phi \to AB\left(\frac{1}{C}\right)=BA\left(\frac{1}{C}\right)$$
12	1 3 4	divrecd	$$⊢\phi \to \frac{A}{C}=A\left(\frac{1}{C}\right)$$
13	12	oveq2d	$$⊢\phi \to B\left(\frac{A}{C}\right)=BA\left(\frac{1}{C}\right)$$
14	11 13	eqtr4d	$$⊢\phi \to AB\left(\frac{1}{C}\right)=B\left(\frac{A}{C}\right)$$