Theorem mdiv

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

	Ref	Expression
Hypotheses	ldiv.a	|- ( ph -> A e. CC )
	ldiv.b	|- ( ph -> B e. CC )
	ldiv.c	|- ( ph -> C e. CC )
	mdiv.an0	|- ( ph -> A =/= 0 )
	mdiv.bn0	|- ( ph -> B =/= 0 )
Assertion	mdiv	|- ( ph -> ( A = ( C / B ) <-> B = ( C / A ) ) )

Proof

Step	Hyp	Ref	Expression
1		ldiv.a	|- ( ph -> A e. CC )
2		ldiv.b	|- ( ph -> B e. CC )
3		ldiv.c	|- ( ph -> C e. CC )
4		mdiv.an0	|- ( ph -> A =/= 0 )
5		mdiv.bn0	|- ( ph -> B =/= 0 )
6	1 2 3 5	ldiv	|- ( ph -> ( ( A x. B ) = C <-> A = ( C / B ) ) )
7	1 2 3 4	rdiv	|- ( ph -> ( ( A x. B ) = C <-> B = ( C / A ) ) )
8	6 7	bitr3d	|- ( ph -> ( A = ( C / B ) <-> B = ( C / A ) ) )