Metamath Proof Explorer

Theorem root1cj

Description: Within the N -th roots of unity, the conjugate of the K -th root is the N - K -th root. (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion root1cj 
|- ( ( N e. NN /\ K e. ZZ ) -> ( * ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) = ( ( -u 1 ^c ( 2 / N ) ) ^ ( N - K ) ) )

Proof

Step Hyp Ref Expression
1 neg1cn 
 |-  -u 1 e. CC
2 2re 
 |-  2 e. RR
3 simpl 
 |-  ( ( N e. NN /\ K e. ZZ ) -> N e. NN )
4 nndivre 
 |-  ( ( 2 e. RR /\ N e. NN ) -> ( 2 / N ) e. RR )
5 2 3 4 sylancr 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( 2 / N ) e. RR )
6 5 recnd 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( 2 / N ) e. CC )
7 cxpcl 
 |-  ( ( -u 1 e. CC /\ ( 2 / N ) e. CC ) -> ( -u 1 ^c ( 2 / N ) ) e. CC )
8 1 6 7 sylancr 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( -u 1 ^c ( 2 / N ) ) e. CC )
9 1 a1i 
 |-  ( ( N e. NN /\ K e. ZZ ) -> -u 1 e. CC )
10 neg1ne0 
 |-  -u 1 =/= 0
11 10 a1i 
 |-  ( ( N e. NN /\ K e. ZZ ) -> -u 1 =/= 0 )
12 9 11 6 cxpne0d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( -u 1 ^c ( 2 / N ) ) =/= 0 )
13 simpr 
 |-  ( ( N e. NN /\ K e. ZZ ) -> K e. ZZ )
14 nnz 
 |-  ( N e. NN -> N e. ZZ )
15 14 adantr 
 |-  ( ( N e. NN /\ K e. ZZ ) -> N e. ZZ )
16 8 12 13 15 expsubd 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ ( N - K ) ) = ( ( ( -u 1 ^c ( 2 / N ) ) ^ N ) / ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) )
17 root1id 
 |-  ( N e. NN -> ( ( -u 1 ^c ( 2 / N ) ) ^ N ) = 1 )
18 17 adantr 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ N ) = 1 )
19 18 oveq1d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( ( -u 1 ^c ( 2 / N ) ) ^ N ) / ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) = ( 1 / ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) )
20 8 12 13 expclzd 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ K ) e. CC )
21 8 12 13 expne0d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ K ) =/= 0 )
22 recval 
 |-  ( ( ( ( -u 1 ^c ( 2 / N ) ) ^ K ) e. CC /\ ( ( -u 1 ^c ( 2 / N ) ) ^ K ) =/= 0 ) -> ( 1 / ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) = ( ( * ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) / ( ( abs ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) ^ 2 ) ) )
23 20 21 22 syl2anc 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( 1 / ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) = ( ( * ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) / ( ( abs ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) ^ 2 ) ) )
24 absexpz 
 |-  ( ( ( -u 1 ^c ( 2 / N ) ) e. CC /\ ( -u 1 ^c ( 2 / N ) ) =/= 0 /\ K e. ZZ ) -> ( abs ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) = ( ( abs ` ( -u 1 ^c ( 2 / N ) ) ) ^ K ) )
25 8 12 13 24 syl3anc 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( abs ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) = ( ( abs ` ( -u 1 ^c ( 2 / N ) ) ) ^ K ) )
26 abscxp2 
 |-  ( ( -u 1 e. CC /\ ( 2 / N ) e. RR ) -> ( abs ` ( -u 1 ^c ( 2 / N ) ) ) = ( ( abs ` -u 1 ) ^c ( 2 / N ) ) )
27 1 5 26 sylancr 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( abs ` ( -u 1 ^c ( 2 / N ) ) ) = ( ( abs ` -u 1 ) ^c ( 2 / N ) ) )
28 ax-1cn 
 |-  1 e. CC
29 28 absnegi 
 |-  ( abs ` -u 1 ) = ( abs ` 1 )
30 abs1 
 |-  ( abs ` 1 ) = 1
31 29 30 eqtri 
 |-  ( abs ` -u 1 ) = 1
32 31 oveq1i 
 |-  ( ( abs ` -u 1 ) ^c ( 2 / N ) ) = ( 1 ^c ( 2 / N ) )
33 27 32 eqtrdi 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( abs ` ( -u 1 ^c ( 2 / N ) ) ) = ( 1 ^c ( 2 / N ) ) )
34 6 1cxpd 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( 1 ^c ( 2 / N ) ) = 1 )
35 33 34 eqtrd 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( abs ` ( -u 1 ^c ( 2 / N ) ) ) = 1 )
36 35 oveq1d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( abs ` ( -u 1 ^c ( 2 / N ) ) ) ^ K ) = ( 1 ^ K ) )
37 1exp 
 |-  ( K e. ZZ -> ( 1 ^ K ) = 1 )
38 37 adantl 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( 1 ^ K ) = 1 )
39 25 36 38 3eqtrd 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( abs ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) = 1 )
40 39 oveq1d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( abs ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) ^ 2 ) = ( 1 ^ 2 ) )
41 sq1 
 |-  ( 1 ^ 2 ) = 1
42 40 41 eqtrdi 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( abs ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) ^ 2 ) = 1 )
43 42 oveq2d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( * ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) / ( ( abs ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) ^ 2 ) ) = ( ( * ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) / 1 ) )
44 20 cjcld 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( * ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) e. CC )
45 44 div1d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( * ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) / 1 ) = ( * ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) )
46 23 43 45 3eqtrd 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( 1 / ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) = ( * ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) )
47 16 19 46 3eqtrrd 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( * ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) = ( ( -u 1 ^c ( 2 / N ) ) ^ ( N - K ) ) )