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 K -1 2 N K = 1 N K

Proof

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