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 ) |
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 ) |