Metamath Proof Explorer

Theorem divmul

Description: Relationship between division and multiplication. (Contributed by NM, 2-Aug-2004) (Revised by Mario Carneiro, 17-Feb-2014)

Ref Expression
Assertion divmul 
|- ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) = B <-> ( C x. B ) = A ) )

Proof

Step Hyp Ref Expression
1 divval 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( A / C ) = ( iota_ x e. CC ( C x. x ) = A ) )
2 1 3expb 
 |-  ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A / C ) = ( iota_ x e. CC ( C x. x ) = A ) )
3 2 3adant2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A / C ) = ( iota_ x e. CC ( C x. x ) = A ) )
4 3 eqeq1d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) = B <-> ( iota_ x e. CC ( C x. x ) = A ) = B ) )
5 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> B e. CC )
6 receu 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> E! x e. CC ( C x. x ) = A )
7 6 3expb 
 |-  ( ( A e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> E! x e. CC ( C x. x ) = A )
8 oveq2 
 |-  ( x = B -> ( C x. x ) = ( C x. B ) )
9 8 eqeq1d 
 |-  ( x = B -> ( ( C x. x ) = A <-> ( C x. B ) = A ) )
10 9 riota2 
 |-  ( ( B e. CC /\ E! x e. CC ( C x. x ) = A ) -> ( ( C x. B ) = A <-> ( iota_ x e. CC ( C x. x ) = A ) = B ) )
11 5 7 10 3imp3i2an 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. B ) = A <-> ( iota_ x e. CC ( C x. x ) = A ) = B ) )
12 4 11 bitr4d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) = B <-> ( C x. B ) = A ) )