Metamath Proof Explorer


Theorem mvlrmuli

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

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

Proof

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