This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )