Description: Property of an N -th root of unity. (Contributed by Mario Carneiro, 23-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | root1id | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neg1cn | |
|
2 | 1 | a1i | |
3 | 2re | |
|
4 | nndivre | |
|
5 | 3 4 | mpan | |
6 | 5 | recnd | |
7 | nnnn0 | |
|
8 | 2 6 7 | cxpmul2d | |
9 | 2cnd | |
|
10 | nncn | |
|
11 | nnne0 | |
|
12 | 9 10 11 | divcan1d | |
13 | 12 | oveq2d | |
14 | 2nn0 | |
|
15 | cxpexp | |
|
16 | 1 14 15 | mp2an | |
17 | ax-1cn | |
|
18 | sqneg | |
|
19 | 17 18 | ax-mp | |
20 | sq1 | |
|
21 | 16 19 20 | 3eqtri | |
22 | 13 21 | eqtrdi | |
23 | 8 22 | eqtr3d | |