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 ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) = 1 ↔ 𝑁 ∥ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 simpl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → 𝑁 ∈ ℕ )
3 nndivre ⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 2 / 𝑁 ) ∈ ℝ )
4 1 2 3 sylancr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 2 / 𝑁 ) ∈ ℝ )
5 4 recnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 2 / 𝑁 ) ∈ ℂ )
6 ax-icn ⊢ i ∈ ℂ
7 picn ⊢ π ∈ ℂ
8 6 7 mulcli ⊢ ( i · π ) ∈ ℂ
9 8 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( i · π ) ∈ ℂ )
10 5 9 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( 2 / 𝑁 ) · ( i · π ) ) ∈ ℂ )
11 efexp ⊢ ( ( ( ( 2 / 𝑁 ) · ( i · π ) ) ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( 𝐾 · ( ( 2 / 𝑁 ) · ( i · π ) ) ) ) = ( ( exp ‘ ( ( 2 / 𝑁 ) · ( i · π ) ) ) ↑ 𝐾 ) )
12 10 11 sylancom ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( 𝐾 · ( ( 2 / 𝑁 ) · ( i · π ) ) ) ) = ( ( exp ‘ ( ( 2 / 𝑁 ) · ( i · π ) ) ) ↑ 𝐾 ) )
13 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
14 13 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℂ )
15 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
16 15 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → 𝑁 ∈ ℂ )
17 2cn ⊢ 2 ∈ ℂ
18 17 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → 2 ∈ ℂ )
19 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
20 19 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → 𝑁 ≠ 0 )
21 14 16 18 20 div32d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 / 𝑁 ) · 2 ) = ( 𝐾 · ( 2 / 𝑁 ) ) )
22 21 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝐾 / 𝑁 ) · 2 ) · ( i · π ) ) = ( ( 𝐾 · ( 2 / 𝑁 ) ) · ( i · π ) ) )
23 14 16 20 divcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 / 𝑁 ) ∈ ℂ )
24 23 18 9 mulassd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝐾 / 𝑁 ) · 2 ) · ( i · π ) ) = ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) )
25 14 5 9 mulassd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · ( 2 / 𝑁 ) ) · ( i · π ) ) = ( 𝐾 · ( ( 2 / 𝑁 ) · ( i · π ) ) ) )
26 22 24 25 3eqtr3d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) = ( 𝐾 · ( ( 2 / 𝑁 ) · ( i · π ) ) ) )
27 26 fveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) ) = ( exp ‘ ( 𝐾 · ( ( 2 / 𝑁 ) · ( i · π ) ) ) ) )
28 neg1cn ⊢ - 1 ∈ ℂ
29 28 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → - 1 ∈ ℂ )
30 neg1ne0 ⊢ - 1 ≠ 0
31 30 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → - 1 ≠ 0 )
32 29 31 5 cxpefd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) = ( exp ‘ ( ( 2 / 𝑁 ) · ( log ‘ - 1 ) ) ) )
33 logm1 ⊢ ( log ‘ - 1 ) = ( i · π )
34 33 oveq2i ⊢ ( ( 2 / 𝑁 ) · ( log ‘ - 1 ) ) = ( ( 2 / 𝑁 ) · ( i · π ) )
35 34 fveq2i ⊢ ( exp ‘ ( ( 2 / 𝑁 ) · ( log ‘ - 1 ) ) ) = ( exp ‘ ( ( 2 / 𝑁 ) · ( i · π ) ) )
36 32 35 eqtrdi ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) = ( exp ‘ ( ( 2 / 𝑁 ) · ( i · π ) ) ) )
37 36 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) = ( ( exp ‘ ( ( 2 / 𝑁 ) · ( i · π ) ) ) ↑ 𝐾 ) )
38 12 27 37 3eqtr4rd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) = ( exp ‘ ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) ) )
39 38 eqeq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) = 1 ↔ ( exp ‘ ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) ) = 1 ) )
40 17 8 mulcli ⊢ ( 2 · ( i · π ) ) ∈ ℂ
41 mulcl ⊢ ( ( ( 𝐾 / 𝑁 ) ∈ ℂ ∧ ( 2 · ( i · π ) ) ∈ ℂ ) → ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) ∈ ℂ )
42 23 40 41 sylancl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) ∈ ℂ )
43 efeq1 ⊢ ( ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) ∈ ℂ → ( ( exp ‘ ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) ) = 1 ↔ ( ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
44 42 43 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( exp ‘ ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) ) = 1 ↔ ( ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ) )
45 6 17 7 mul12i ⊢ ( i · ( 2 · π ) ) = ( 2 · ( i · π ) )
46 45 oveq2i ⊢ ( ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) / ( i · ( 2 · π ) ) ) = ( ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) / ( 2 · ( i · π ) ) )
47 40 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 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 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 2 · ( i · π ) ) ≠ 0 )
56 23 47 55 divcan4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) / ( 2 · ( i · π ) ) ) = ( 𝐾 / 𝑁 ) )
57 46 56 syl5eq ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) / ( i · ( 2 · π ) ) ) = ( 𝐾 / 𝑁 ) )
58 57 eleq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ↔ ( 𝐾 / 𝑁 ) ∈ ℤ ) )
59 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
60 59 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → 𝑁 ∈ ℤ )
61 simpr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℤ )
62 dvdsval2 ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ 𝐾 ∈ ℤ ) → ( 𝑁 ∥ 𝐾 ↔ ( 𝐾 / 𝑁 ) ∈ ℤ ) )
63 60 20 61 62 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 ∥ 𝐾 ↔ ( 𝐾 / 𝑁 ) ∈ ℤ ) )
64 58 63 bitr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( ( 𝐾 / 𝑁 ) · ( 2 · ( i · π ) ) ) / ( i · ( 2 · π ) ) ) ∈ ℤ ↔ 𝑁 ∥ 𝐾 ) )
65 39 44 64 3bitrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝐾 ) = 1 ↔ 𝑁 ∥ 𝐾 ) )