let n be non zero Element of NAT ; :: thesis: for k being Element of NAT
for x being Element of (MultGroup F_Complex) 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 (MultGroup F_Complex) 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 (MultGroup F_Complex); :: 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 A4, Th24;
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 NAT_D:2, NEWTON:58;
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 A6, NAT_D:def 1;
A11: for m being Nat st x |^ m = 1_ (MultGroup F_Complex) & m <> 0 holds
n div kgn <= m

proof

let m be Nat; :: thesis: ( x |^ m = 1_ (MultGroup F_Complex) & m <> 0 implies n div kgn <= m )
assume that
A12: x |^ m = 1_ (MultGroup F_Complex) 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 A6, A17;
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 A17, A18, A16;
then m * a = ((j * b) * kgn) / kgn by A6, XCMPLX_1:89;
then m * a = j * b by A6, XCMPLX_1:89;
then A20: bi divides m * ai by NAT_D:def 3;
m < bi by A6, A10, A14, A18, NAT_D:18;
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 COMPTRIG:5, NAT_D:1, XREAL_1:68;
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_ (MultGroup F_Complex) = [**1,0**] by Th17, COMPLFLD:8;
x |^ m = (power F_Complex) . (y,m) by Th29
.= y |^ m by COMPLFLD:74
.= [**(cos (((2 * PI) * (k * m)) / n)),(sin ((((2 * PI) * k) * m) / n))**] by A4, A21, COMPTRIG:53
.= [**(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 A12, A23, COMPLEX1:77;
hence contradiction by A15, A22, COMPTRIG:5, COMPTRIG:61; :: thesis: verum

end;

hence n div kgn <= m by A6, A9, NAT_D:def 1; :: 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 A3, XCMPLX_1:82
.= (((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) = (power F_Complex) . (y,vn) by A10, Th29
.= y |^ vn by COMPLFLD:74
.= [**(cos ((((2 * PI) * k) / n) * vn)),(sin ((((2 * PI) * k) / n) * vn))**] by A4, COMPTRIG:53
.= [**(cos 0),(sin (((2 * PI) * i) + 0))**] by A24, COMPLEX2:9
.= 1 + (0 * <i>) by COMPLEX2:8, SIN_COS:31
.= 1_ (MultGroup F_Complex) by Th17, COMPLFLD:8 ;
hence ord x = n div (k gcd n) by A7, A5, A11, GROUP_1:def 11; :: thesis: verum