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 𝐴 ∈ ℂ
mvlrmuli.2 𝐵 ∈ ℂ
mvlrmuli.3 𝐵 ≠ 0
mvlrmuli.4 ( 𝐴 · 𝐵 ) = 𝐶
Assertion mvlrmuli 𝐴 = ( 𝐶 / 𝐵 )

Proof

Step Hyp Ref Expression
1 mvlrmuli.1 𝐴 ∈ ℂ
2 mvlrmuli.2 𝐵 ∈ ℂ
3 mvlrmuli.3 𝐵 ≠ 0
4 mvlrmuli.4 ( 𝐴 · 𝐵 ) = 𝐶
5 1 2 3 divcan4i ( ( 𝐴 · 𝐵 ) / 𝐵 ) = 𝐴
6 4 oveq1i ( ( 𝐴 · 𝐵 ) / 𝐵 ) = ( 𝐶 / 𝐵 )
7 5 6 eqtr3i 𝐴 = ( 𝐶 / 𝐵 )