Metamath Proof Explorer


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 )