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

Metamath Proof Explorer

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 ) )