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-12NN=1

Proof

Step Hyp Ref Expression
1 neg1cn 1
2 1 a1i N1
3 2re 2
4 nndivre 2N2N
5 3 4 mpan N2N
6 5 recnd N2N
7 nnnn0 NN0
8 2 6 7 cxpmul2d N12N N=-12NN
9 2cnd N2
10 nncn NN
11 nnne0 NN0
12 9 10 11 divcan1d N2N N=2
13 12 oveq2d N12N N=12
14 2nn0 20
15 cxpexp 12012=12
16 1 14 15 mp2an 12=12
17 ax-1cn 1
18 sqneg 112=12
19 17 18 ax-mp 12=12
20 sq1 12=1
21 16 19 20 3eqtri 12=1
22 13 21 eqtrdi N12N N=1
23 8 22 eqtr3d N-12NN=1