Metamath Proof Explorer

Theorem cjdiv

Description: Complex conjugate distributes over division. (Contributed by NM, 29-Apr-2005) (Proof shortened by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion cjdiv 
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( * ` ( A / B ) ) = ( ( * ` A ) / ( * ` B ) ) )

Proof

Step Hyp Ref Expression
1 divcl 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) e. CC )
2 cjcl 
 |-  ( ( A / B ) e. CC -> ( * ` ( A / B ) ) e. CC )
3 1 2 syl 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( * ` ( A / B ) ) e. CC )
4 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> B e. CC )
5 cjcl 
 |-  ( B e. CC -> ( * ` B ) e. CC )
6 4 5 syl 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( * ` B ) e. CC )
7 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> B =/= 0 )
8 cjne0 
 |-  ( B e. CC -> ( B =/= 0 <-> ( * ` B ) =/= 0 ) )
9 4 8 syl 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B =/= 0 <-> ( * ` B ) =/= 0 ) )
10 7 9 mpbid 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( * ` B ) =/= 0 )
11 3 6 10 divcan4d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( ( * ` ( A / B ) ) x. ( * ` B ) ) / ( * ` B ) ) = ( * ` ( A / B ) ) )
12 cjmul 
 |-  ( ( ( A / B ) e. CC /\ B e. CC ) -> ( * ` ( ( A / B ) x. B ) ) = ( ( * ` ( A / B ) ) x. ( * ` B ) ) )
13 1 4 12 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( * ` ( ( A / B ) x. B ) ) = ( ( * ` ( A / B ) ) x. ( * ` B ) ) )
14 divcan1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) x. B ) = A )
15 14 fveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( * ` ( ( A / B ) x. B ) ) = ( * ` A ) )
16 13 15 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( * ` ( A / B ) ) x. ( * ` B ) ) = ( * ` A ) )
17 16 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( ( * ` ( A / B ) ) x. ( * ` B ) ) / ( * ` B ) ) = ( ( * ` A ) / ( * ` B ) ) )
18 11 17 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( * ` ( A / B ) ) = ( ( * ` A ) / ( * ` B ) ) )