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	eqtrid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ ) → ( ( ( 𝐾 / 𝑁 ) · ( 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 ↔ 𝑁 ∥ 𝐾 ) )