Metamath Proof Explorer

Theorem div11

Description: One-to-one relationship for division. (Contributed by NM, 20-Apr-2006) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> A e. CC )
2 simp3l 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> C e. CC )
3 simp3r 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> C =/= 0 )
4 divcl 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( A / C ) e. CC )
5 1 2 3 4 syl3anc 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A / C ) e. CC )
6 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> B e. CC )
7 divcl 
 |-  ( ( B e. CC /\ C e. CC /\ C =/= 0 ) -> ( B / C ) e. CC )
8 6 2 3 7 syl3anc 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( B / C ) e. CC )
9 5 8 2 3 mulcand 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. ( A / C ) ) = ( C x. ( B / C ) ) <-> ( A / C ) = ( B / C ) ) )
10 divcan2 
 |-  ( ( A e. CC /\ C e. CC /\ C =/= 0 ) -> ( C x. ( A / C ) ) = A )
11 1 2 3 10 syl3anc 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( C x. ( A / C ) ) = A )
12 divcan2 
 |-  ( ( B e. CC /\ C e. CC /\ C =/= 0 ) -> ( C x. ( B / C ) ) = B )
13 6 2 3 12 syl3anc 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( C x. ( B / C ) ) = B )
14 11 13 eqeq12d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( C x. ( A / C ) ) = ( C x. ( B / C ) ) <-> A = B ) )
15 9 14 bitr3d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) = ( B / C ) <-> A = B ) )