Metamath Proof Explorer


Theorem mvllmuli

Description: Move the left term in a product on the LHS to the RHS, inference form. Uses divcan4i . (Contributed by David A. Wheeler, 11-Oct-2018)

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

Proof

Step Hyp Ref Expression
1 mvllmuli.1
 |-  A e. CC
2 mvllmuli.2
 |-  B e. CC
3 mvllmuli.3
 |-  A =/= 0
4 mvllmuli.4
 |-  ( A x. B ) = C
5 2 1 3 divcan4i
 |-  ( ( B x. A ) / A ) = B
6 1 2 4 mulcomli
 |-  ( B x. A ) = C
7 6 oveq1i
 |-  ( ( B x. A ) / A ) = ( C / A )
8 5 7 eqtr3i
 |-  B = ( C / A )