Theorem root1id

Description: Property of an N -th root of unity. (Contributed by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Assertion	root1id	⊢ ( 𝑁 ∈ ℕ → ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑁 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		neg1cn	⊢ - 1 ∈ ℂ
2	1	a1i	⊢ ( 𝑁 ∈ ℕ → - 1 ∈ ℂ )
3		2re	⊢ 2 ∈ ℝ
4		nndivre	⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℕ ) → ( 2 / 𝑁 ) ∈ ℝ )
5	3 4	mpan	⊢ ( 𝑁 ∈ ℕ → ( 2 / 𝑁 ) ∈ ℝ )
6	5	recnd	⊢ ( 𝑁 ∈ ℕ → ( 2 / 𝑁 ) ∈ ℂ )
7		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
8	2 6 7	cxpmul2d	⊢ ( 𝑁 ∈ ℕ → ( - 1 ↑𝑐 ( ( 2 / 𝑁 ) · 𝑁 ) ) = ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑁 ) )
9		2cnd	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
10		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
11		nnne0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
12	9 10 11	divcan1d	⊢ ( 𝑁 ∈ ℕ → ( ( 2 / 𝑁 ) · 𝑁 ) = 2 )
13	12	oveq2d	⊢ ( 𝑁 ∈ ℕ → ( - 1 ↑𝑐 ( ( 2 / 𝑁 ) · 𝑁 ) ) = ( - 1 ↑𝑐 2 ) )
14		2nn0	⊢ 2 ∈ ℕ0
15		cxpexp	⊢ ( ( - 1 ∈ ℂ ∧ 2 ∈ ℕ0 ) → ( - 1 ↑𝑐 2 ) = ( - 1 ↑ 2 ) )
16	1 14 15	mp2an	⊢ ( - 1 ↑𝑐 2 ) = ( - 1 ↑ 2 )
17		ax-1cn	⊢ 1 ∈ ℂ
18		sqneg	⊢ ( 1 ∈ ℂ → ( - 1 ↑ 2 ) = ( 1 ↑ 2 ) )
19	17 18	ax-mp	⊢ ( - 1 ↑ 2 ) = ( 1 ↑ 2 )
20		sq1	⊢ ( 1 ↑ 2 ) = 1
21	16 19 20	3eqtri	⊢ ( - 1 ↑𝑐 2 ) = 1
22	13 21	eqtrdi	⊢ ( 𝑁 ∈ ℕ → ( - 1 ↑𝑐 ( ( 2 / 𝑁 ) · 𝑁 ) ) = 1 )
23	8 22	eqtr3d	⊢ ( 𝑁 ∈ ℕ → ( ( - 1 ↑𝑐 ( 2 / 𝑁 ) ) ↑ 𝑁 ) = 1 )