Theorem ldiv

Description: Left-division. (Contributed by BJ, 6-Jun-2019)

	Ref	Expression
Hypotheses	ldiv.a	$$⊢\phi \to A\in ℂ$$
	ldiv.b	$$⊢\phi \to B\in ℂ$$
	ldiv.c	$$⊢\phi \to C\in ℂ$$
	ldiv.bn0	$$⊢\phi \to B\ne 0$$
Assertion	ldiv	$$⊢\phi \to \left(AB=C\leftrightarrow A=\frac{C}{B}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ldiv.a	$$⊢\phi \to A\in ℂ$$
2		ldiv.b	$$⊢\phi \to B\in ℂ$$
3		ldiv.c	$$⊢\phi \to C\in ℂ$$
4		ldiv.bn0	$$⊢\phi \to B\ne 0$$
5		oveq1	$$⊢AB=C\to \frac{AB}{B}=\frac{C}{B}$$
6	1 2 4	divcan4d	$$⊢\phi \to \frac{AB}{B}=A$$
7	6	eqeq1d	$$⊢\phi \to \left(\frac{AB}{B}=\frac{C}{B}\leftrightarrow A=\frac{C}{B}\right)$$
8	5 7	syl5ib	$$⊢\phi \to \left(AB=C\to A=\frac{C}{B}\right)$$
9		oveq1	$$⊢A=\frac{C}{B}\to AB=\left(\frac{C}{B}\right)B$$
10	3 2 4	divcan1d	$$⊢\phi \to \left(\frac{C}{B}\right)B=C$$
11	10	eqeq2d	$$⊢\phi \to \left(AB=\left(\frac{C}{B}\right)B\leftrightarrow AB=C\right)$$
12	9 11	syl5ib	$$⊢\phi \to \left(A=\frac{C}{B}\to AB=C\right)$$
13	8 12	impbid	$$⊢\phi \to \left(AB=C\leftrightarrow A=\frac{C}{B}\right)$$