let n be non zero Element of NAT ; :: thesis: for k being Element of NAT
for x being Element of st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] holds
ord x = n div (k gcd n)

let k be Element of NAT ; :: thesis: for x being Element of st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] holds
ord x = n div (k gcd n)

reconsider kgn = k gcd n as Element of NAT ;
A1: k gcd n divides n by INT_2:21;
then consider vn being Nat such that
A2: n = kgn * vn by NAT_D:def 3;
k gcd n divides k by INT_2:21;
then consider i being Nat such that
A3: k = kgn * i by NAT_D:def 3;
let x be Element of ; :: thesis: ( x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] implies ord x = n div (k gcd n) )
assume A4: x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] ; :: thesis: ord x = n div (k gcd n)
x in n -roots_of_1 by ;
then A5: not x is being_of_order_0 by Th30;
A6: n gcd k > 0 by NEWTON:58;
A7: now :: thesis: not n div kgn = 0
assume n div kgn = 0 ; :: thesis: contradiction
then n = (kgn * 0) + (n mod kgn) by ;
hence contradiction by A1, A6, NAT_D:1, NAT_D:7; :: thesis: verum
end;
reconsider y = x as Element of F_Complex by Th19;
reconsider vn = vn as Element of NAT by ORDINAL1:def 12;
A9: n = (kgn * vn) + 0 by A2;
then A10: n div kgn = vn by ;
A11: for m being Nat st x |^ m = 1_ & m <> 0 holds
n div kgn <= m
proof
let m be Nat; :: thesis: ( x |^ m = 1_ & m <> 0 implies n div kgn <= m )
assume that
A12: x |^ m = 1_ and
A13: m <> 0 ; :: thesis: n div kgn <= m
reconsider m = m as Element of NAT by ORDINAL1:def 12;
now :: thesis: not m < vn
assume A14: m < vn ; :: thesis: contradiction
A15: now :: thesis: not (k * m) mod n = 0
assume (k * m) mod n = 0 ; :: thesis: contradiction
then n divides k * m by PEPIN:6;
then consider j being Nat such that
A16: k * m = n * j by NAT_D:def 3;
consider a, b being Integer such that
A17: k = kgn * a and
A18: n = kgn * b and
A19: a,b are_coprime by INT_2:23;
0 <= a by ;
then reconsider ai = a as Element of NAT by INT_1:3;
0 <= b by A18;
then reconsider bi = b as Element of NAT by INT_1:3;
(m * a) * kgn = j * (b * kgn) by ;
then m * a = ((j * b) * kgn) / kgn by ;
then m * a = j * b by ;
then A20: bi divides m * ai by NAT_D:def 3;
m < bi by ;
hence contradiction by A13, A19, A20, INT_2:25, NAT_D:7; :: thesis: verum
end;
A21: (((2 * PI) * k) / n) * m = ((2 * PI) * k) / (n / m) by XCMPLX_1:82
.= (((2 * PI) * k) * m) / n by XCMPLX_1:77 ;
(2 * PI) * ((k * m) mod n) < (2 * PI) * n by ;
then ((2 * PI) * ((k * m) mod n)) / n < ((2 * PI) * n) / n by XREAL_1:74;
then A22: ((2 * PI) * ((k * m) mod n)) / n < 2 * PI by XCMPLX_1:89;
A23: 1_ = [**1,0**] by ;
x |^ m = . (y,m) by Th29
.= y |^ m by COMPLFLD:74
.= [**(cos (((2 * PI) * (k * m)) / n)),(sin ((((2 * PI) * k) * m) / n))**] by
.= [**(cos (((2 * PI) * ((k * m) mod n)) / n)),(sin (((2 * PI) * ((k * m) mod n)) / n))**] by Th10 ;
then cos (((2 * PI) * ((k * m) mod n)) / n) = 1 by ;
hence contradiction by A15, A22, COMPTRIG:5, COMPTRIG:61; :: thesis: verum
end;
hence n div kgn <= m by ; :: thesis: verum
end;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A24: (((2 * PI) * k) / n) * vn = ((2 * PI) * (kgn * i)) / (n / vn) by
.= (((2 * PI) * (kgn * i)) * vn) / n by XCMPLX_1:77
.= (((2 * PI) * i) * n) / n by A2
.= ((2 * PI) * i) + 0 by XCMPLX_1:89 ;
x |^ (n div kgn) = . (y,vn) by
.= y |^ vn by COMPLFLD:74
.= [**(cos ((((2 * PI) * k) / n) * vn)),(sin ((((2 * PI) * k) / n) * vn))**] by
.= [**(),(sin (((2 * PI) * i) + 0))**] by
.= 1 + () by
.= 1_ by ;
hence ord x = n div (k gcd n) by ; :: thesis: verum