Metamath Proof Explorer

Theorem root1eq1

Description: The only powers of an N -th root of unity that equal 1 are the multiples of N . In other words, -u 1 ^c ( 2 / N ) has order N in the multiplicative group of nonzero complex numbers. (In fact, these and their powers are the only elements of finite order in the complex numbers.) (Contributed by Mario Carneiro, 28-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 simpl 
 |-  ( ( N e. NN /\ K e. ZZ ) -> N e. NN )
3 nndivre 
 |-  ( ( 2 e. RR /\ N e. NN ) -> ( 2 / N ) e. RR )
4 1 2 3 sylancr 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( 2 / N ) e. RR )
5 4 recnd 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( 2 / N ) e. CC )
6 ax-icn 
 |-  _i e. CC
7 picn 
 |-  _pi e. CC
8 6 7 mulcli 
 |-  ( _i x. _pi ) e. CC
9 8 a1i 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( _i x. _pi ) e. CC )
10 5 9 mulcld 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( 2 / N ) x. ( _i x. _pi ) ) e. CC )
11 efexp 
 |-  ( ( ( ( 2 / N ) x. ( _i x. _pi ) ) e. CC /\ K e. ZZ ) -> ( exp ` ( K x. ( ( 2 / N ) x. ( _i x. _pi ) ) ) ) = ( ( exp ` ( ( 2 / N ) x. ( _i x. _pi ) ) ) ^ K ) )
12 10 11 sylancom 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( exp ` ( K x. ( ( 2 / N ) x. ( _i x. _pi ) ) ) ) = ( ( exp ` ( ( 2 / N ) x. ( _i x. _pi ) ) ) ^ K ) )
13 zcn 
 |-  ( K e. ZZ -> K e. CC )
14 13 adantl 
 |-  ( ( N e. NN /\ K e. ZZ ) -> K e. CC )
15 nncn 
 |-  ( N e. NN -> N e. CC )
16 15 adantr 
 |-  ( ( N e. NN /\ K e. ZZ ) -> N e. CC )
17 2cn 
 |-  2 e. CC
18 17 a1i 
 |-  ( ( N e. NN /\ K e. ZZ ) -> 2 e. CC )
19 nnne0 
 |-  ( N e. NN -> N =/= 0 )
20 19 adantr 
 |-  ( ( N e. NN /\ K e. ZZ ) -> N =/= 0 )
21 14 16 18 20 div32d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( K / N ) x. 2 ) = ( K x. ( 2 / N ) ) )
22 21 oveq1d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( ( K / N ) x. 2 ) x. ( _i x. _pi ) ) = ( ( K x. ( 2 / N ) ) x. ( _i x. _pi ) ) )
23 14 16 20 divcld 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( K / N ) e. CC )
24 23 18 9 mulassd 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( ( K / N ) x. 2 ) x. ( _i x. _pi ) ) = ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) )
25 14 5 9 mulassd 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( K x. ( 2 / N ) ) x. ( _i x. _pi ) ) = ( K x. ( ( 2 / N ) x. ( _i x. _pi ) ) ) )
26 22 24 25 3eqtr3d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) = ( K x. ( ( 2 / N ) x. ( _i x. _pi ) ) ) )
27 26 fveq2d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( exp ` ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) ) = ( exp ` ( K x. ( ( 2 / N ) x. ( _i x. _pi ) ) ) ) )
28 neg1cn 
 |-  -u 1 e. CC
29 28 a1i 
 |-  ( ( N e. NN /\ K e. ZZ ) -> -u 1 e. CC )
30 neg1ne0 
 |-  -u 1 =/= 0
31 30 a1i 
 |-  ( ( N e. NN /\ K e. ZZ ) -> -u 1 =/= 0 )
32 29 31 5 cxpefd 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( -u 1 ^c ( 2 / N ) ) = ( exp ` ( ( 2 / N ) x. ( log ` -u 1 ) ) ) )
33 logm1 
 |-  ( log ` -u 1 ) = ( _i x. _pi )
34 33 oveq2i 
 |-  ( ( 2 / N ) x. ( log ` -u 1 ) ) = ( ( 2 / N ) x. ( _i x. _pi ) )
35 34 fveq2i 
 |-  ( exp ` ( ( 2 / N ) x. ( log ` -u 1 ) ) ) = ( exp ` ( ( 2 / N ) x. ( _i x. _pi ) ) )
36 32 35 eqtrdi 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( -u 1 ^c ( 2 / N ) ) = ( exp ` ( ( 2 / N ) x. ( _i x. _pi ) ) ) )
37 36 oveq1d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ K ) = ( ( exp ` ( ( 2 / N ) x. ( _i x. _pi ) ) ) ^ K ) )
38 12 27 37 3eqtr4rd 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( -u 1 ^c ( 2 / N ) ) ^ K ) = ( exp ` ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) ) )
39 38 eqeq1d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( ( -u 1 ^c ( 2 / N ) ) ^ K ) = 1 <-> ( exp ` ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) ) = 1 ) )
40 17 8 mulcli 
 |-  ( 2 x. ( _i x. _pi ) ) e. CC
41 mulcl 
 |-  ( ( ( K / N ) e. CC /\ ( 2 x. ( _i x. _pi ) ) e. CC ) -> ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) e. CC )
42 23 40 41 sylancl 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) e. CC )
43 efeq1 
 |-  ( ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) e. CC -> ( ( exp ` ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) ) = 1 <-> ( ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
44 42 43 syl 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( exp ` ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) ) = 1 <-> ( ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
45 6 17 7 mul12i 
 |-  ( _i x. ( 2 x. _pi ) ) = ( 2 x. ( _i x. _pi ) )
46 45 oveq2i 
 |-  ( ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) / ( _i x. ( 2 x. _pi ) ) ) = ( ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) / ( 2 x. ( _i x. _pi ) ) )
47 40 a1i 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( 2 x. ( _i x. _pi ) ) e. CC )
48 2ne0 
 |-  2 =/= 0
49 ine0 
 |-  _i =/= 0
50 pire 
 |-  _pi e. RR
51 pipos 
 |-  0 < _pi
52 50 51 gt0ne0ii 
 |-  _pi =/= 0
53 6 7 49 52 mulne0i 
 |-  ( _i x. _pi ) =/= 0
54 17 8 48 53 mulne0i 
 |-  ( 2 x. ( _i x. _pi ) ) =/= 0
55 54 a1i 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( 2 x. ( _i x. _pi ) ) =/= 0 )
56 23 47 55 divcan4d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) / ( 2 x. ( _i x. _pi ) ) ) = ( K / N ) )
57 46 56 syl5eq 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) / ( _i x. ( 2 x. _pi ) ) ) = ( K / N ) )
58 57 eleq1d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ <-> ( K / N ) e. ZZ ) )
59 nnz 
 |-  ( N e. NN -> N e. ZZ )
60 59 adantr 
 |-  ( ( N e. NN /\ K e. ZZ ) -> N e. ZZ )
61 simpr 
 |-  ( ( N e. NN /\ K e. ZZ ) -> K e. ZZ )
62 dvdsval2 
 |-  ( ( N e. ZZ /\ N =/= 0 /\ K e. ZZ ) -> ( N || K <-> ( K / N ) e. ZZ ) )
63 60 20 61 62 syl3anc 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( N || K <-> ( K / N ) e. ZZ ) )
64 58 63 bitr4d 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( ( ( K / N ) x. ( 2 x. ( _i x. _pi ) ) ) / ( _i x. ( 2 x. _pi ) ) ) e. ZZ <-> N || K ) )
65 39 44 64 3bitrd 
 |-  ( ( N e. NN /\ K e. ZZ ) -> ( ( ( -u 1 ^c ( 2 / N ) ) ^ K ) = 1 <-> N || K ) )