Theorem divcan8d

Description: A cancellation law for division. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	divcan8d.a	|- ( ph -> A e. CC )
	divcan8d.b	|- ( ph -> B e. CC )
	divcan8d.a0	|- ( ph -> A =/= 0 )
	divcan8d.b0	|- ( ph -> B =/= 0 )
Assertion	divcan8d	|- ( ph -> ( B / ( A x. B ) ) = ( 1 / A ) )

Proof

Step	Hyp	Ref	Expression
1		divcan8d.a	|- ( ph -> A e. CC )
2		divcan8d.b	|- ( ph -> B e. CC )
3		divcan8d.a0	|- ( ph -> A =/= 0 )
4		divcan8d.b0	|- ( ph -> B =/= 0 )
5	1 2	mulcld	|- ( ph -> ( A x. B ) e. CC )
6	1 2 3 4	mulne0d	|- ( ph -> ( A x. B ) =/= 0 )
7	1 2 6	mulne0bbd	|- ( ph -> B =/= 0 )
8	2 5 2 6 7	divcan7d	|- ( ph -> ( ( B / B ) / ( ( A x. B ) / B ) ) = ( B / ( A x. B ) ) )
9	8	eqcomd	|- ( ph -> ( B / ( A x. B ) ) = ( ( B / B ) / ( ( A x. B ) / B ) ) )
10	2 4	dividd	|- ( ph -> ( B / B ) = 1 )
11	1 2 4	divcan4d	|- ( ph -> ( ( A x. B ) / B ) = A )
12	10 11	oveq12d	|- ( ph -> ( ( B / B ) / ( ( A x. B ) / B ) ) = ( 1 / A ) )
13		eqidd	|- ( ph -> ( 1 / A ) = ( 1 / A ) )
14	9 12 13	3eqtrd	|- ( ph -> ( B / ( A x. B ) ) = ( 1 / A ) )