Theorem divval

Description: Value of division: if A and B are complex numbers with B nonzero, then ( A / B ) is the (unique) complex number such that ( B x. x ) = A . (Contributed by NM, 8-May-1999) (Revised by Mario Carneiro, 17-Feb-2014)

	Ref	Expression
Assertion	divval	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( iota_ x e. CC ( B x. x ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	|- ( B e. ( CC \ { 0 } ) <-> ( B e. CC /\ B =/= 0 ) )
2		eqeq2	|- ( z = A -> ( ( y x. x ) = z <-> ( y x. x ) = A ) )
3	2	riotabidv	|- ( z = A -> ( iota_ x e. CC ( y x. x ) = z ) = ( iota_ x e. CC ( y x. x ) = A ) )
4		oveq1	|- ( y = B -> ( y x. x ) = ( B x. x ) )
5	4	eqeq1d	|- ( y = B -> ( ( y x. x ) = A <-> ( B x. x ) = A ) )
6	5	riotabidv	|- ( y = B -> ( iota_ x e. CC ( y x. x ) = A ) = ( iota_ x e. CC ( B x. x ) = A ) )
7		df-div	|- / = ( z e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ x e. CC ( y x. x ) = z ) )
8		riotaex	|- ( iota_ x e. CC ( B x. x ) = A ) e. _V
9	3 6 7 8	ovmpo	|- ( ( A e. CC /\ B e. ( CC \ { 0 } ) ) -> ( A / B ) = ( iota_ x e. CC ( B x. x ) = A ) )
10	1 9	sylan2br	|- ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( A / B ) = ( iota_ x e. CC ( B x. x ) = A ) )
11	10	3impb	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( iota_ x e. CC ( B x. x ) = A ) )