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