Theorem root1id

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

	Ref	Expression
Assertion	root1id	|- ( N e. NN -> ( ( -u 1 ^c ( 2 / N ) ) ^ N ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		neg1cn	|- -u 1 e. CC
2	1	a1i	|- ( N e. NN -> -u 1 e. CC )
3		2re	|- 2 e. RR
4		nndivre	|- ( ( 2 e. RR /\ N e. NN ) -> ( 2 / N ) e. RR )
5	3 4	mpan	|- ( N e. NN -> ( 2 / N ) e. RR )
6	5	recnd	|- ( N e. NN -> ( 2 / N ) e. CC )
7		nnnn0	|- ( N e. NN -> N e. NN0 )
8	2 6 7	cxpmul2d	|- ( N e. NN -> ( -u 1 ^c ( ( 2 / N ) x. N ) ) = ( ( -u 1 ^c ( 2 / N ) ) ^ N ) )
9		2cnd	|- ( N e. NN -> 2 e. CC )
10		nncn	|- ( N e. NN -> N e. CC )
11		nnne0	|- ( N e. NN -> N =/= 0 )
12	9 10 11	divcan1d	|- ( N e. NN -> ( ( 2 / N ) x. N ) = 2 )
13	12	oveq2d	|- ( N e. NN -> ( -u 1 ^c ( ( 2 / N ) x. N ) ) = ( -u 1 ^c 2 ) )
14		2nn0	|- 2 e. NN0
15		cxpexp	|- ( ( -u 1 e. CC /\ 2 e. NN0 ) -> ( -u 1 ^c 2 ) = ( -u 1 ^ 2 ) )
16	1 14 15	mp2an	|- ( -u 1 ^c 2 ) = ( -u 1 ^ 2 )
17		ax-1cn	|- 1 e. CC
18		sqneg	|- ( 1 e. CC -> ( -u 1 ^ 2 ) = ( 1 ^ 2 ) )
19	17 18	ax-mp	|- ( -u 1 ^ 2 ) = ( 1 ^ 2 )
20		sq1	|- ( 1 ^ 2 ) = 1
21	16 19 20	3eqtri	|- ( -u 1 ^c 2 ) = 1
22	13 21	eqtrdi	|- ( N e. NN -> ( -u 1 ^c ( ( 2 / N ) x. N ) ) = 1 )
23	8 22	eqtr3d	|- ( N e. NN -> ( ( -u 1 ^c ( 2 / N ) ) ^ N ) = 1 )