Theorem lcmineqlem5

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

	Ref	Expression
Hypotheses	lcmineqlem5.1	|- ( ph -> A e. CC )
	lcmineqlem5.2	|- ( ph -> B e. CC )
	lcmineqlem5.3	|- ( ph -> C e. CC )
	lcmineqlem5.4	|- ( ph -> C =/= 0 )
Assertion	lcmineqlem5	|- ( ph -> ( A x. ( B x. ( 1 / C ) ) ) = ( B x. ( A / C ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem5.1	|- ( ph -> A e. CC )
2		lcmineqlem5.2	|- ( ph -> B e. CC )
3		lcmineqlem5.3	|- ( ph -> C e. CC )
4		lcmineqlem5.4	|- ( ph -> C =/= 0 )
5	3 4	reccld	|- ( ph -> ( 1 / C ) e. CC )
6	1 2 5	mulassd	|- ( ph -> ( ( A x. B ) x. ( 1 / C ) ) = ( A x. ( B x. ( 1 / C ) ) ) )
7	1 2	mulcomd	|- ( ph -> ( A x. B ) = ( B x. A ) )
8	7	oveq1d	|- ( ph -> ( ( A x. B ) x. ( 1 / C ) ) = ( ( B x. A ) x. ( 1 / C ) ) )
9	6 8	eqtr3d	|- ( ph -> ( A x. ( B x. ( 1 / C ) ) ) = ( ( B x. A ) x. ( 1 / C ) ) )
10	2 1 5	mulassd	|- ( ph -> ( ( B x. A ) x. ( 1 / C ) ) = ( B x. ( A x. ( 1 / C ) ) ) )
11	9 10	eqtrd	|- ( ph -> ( A x. ( B x. ( 1 / C ) ) ) = ( B x. ( A x. ( 1 / C ) ) ) )
12	1 3 4	divrecd	|- ( ph -> ( A / C ) = ( A x. ( 1 / C ) ) )
13	12	oveq2d	|- ( ph -> ( B x. ( A / C ) ) = ( B x. ( A x. ( 1 / C ) ) ) )
14	11 13	eqtr4d	|- ( ph -> ( A x. ( B x. ( 1 / C ) ) ) = ( B x. ( A / C ) ) )