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 \in ℕ \land K \in ℤ) \to ({({-1}^{\frac{2}{N}})}^{K} = 1 \leftrightarrow N ∥ K)$

Proof

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

Metamath Proof Explorer

Theorem root1eq1

Proof