This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℂ$
	mvllmuli.2	$⊢ B \in ℂ$
	mvllmuli.3	$⊢ A \neq 0$
	mvllmuli.4	$⊢ A B = C$
Assertion	mvllmuli	$⊢ B = \frac{C}{A}$

Proof

Step	Hyp	Ref	Expression
1		mvllmuli.1	$⊢ A \in ℂ$
2		mvllmuli.2	$⊢ B \in ℂ$
3		mvllmuli.3	$⊢ A \neq 0$
4		mvllmuli.4	$⊢ A B = C$
5	2 1 3	divcan4i	$⊢ \frac{B A}{A} = B$
6	1 2 4	mulcomli	$⊢ B A = C$
7	6	oveq1i	$⊢ \frac{B A}{A} = \frac{C}{A}$
8	5 7	eqtr3i	$⊢ B = \frac{C}{A}$