let n be non empty 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:31;
then consider vn being Nat such that
A2: n = kgn * vn by NAT_D:def 3;
k gcd n divides k by INT_2:31;
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, Th27;
then A5: not x is being_of_order_0 by Th33;
A6: n gcd k > 0 by NEWTON:71;

A7: now

assume n div kgn = 0 ; :: thesis: contradiction
then n = (kgn * 0) + (n mod kgn) by NAT_D:2, NEWTON:71;
hence contradiction by A1, A6, NAT_D:1, NAT_D:7; :: thesis: verum

end;

reconsider y = x as Element of F_Complex by Th22;
reconsider vn = vn as Element of NAT by ORDINAL1:def 13;
A8: not vn is empty by A2;
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 13;

now

assume A14: m < vn ; :: thesis: contradiction

A15: now

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_relative_prime by INT_2:38;
0 <= a by A6, A17;
then reconsider ai = a as Element of NAT by INT_1:16;
0 <= b by A18;
then reconsider bi = b as Element of NAT by INT_1:16;
(m * a) * kgn = j * (b * kgn) by A17, A18, A16;
then m * a = ((j * b) * kgn) / kgn by A6, XCMPLX_1:90;
then m * a = j * b by A6, XCMPLX_1:90;
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:40, NAT_D:7; :: thesis: verum

end;

A21: (((2 * PI) * k) / n) * m = ((2 * PI) * k) / (n / m) by XCMPLX_1:83
.= (((2 * PI) * k) * m) / n by XCMPLX_1:78 ;
(2 * PI) * ((k * m) mod n) < (2 * PI) * n by COMPTRIG:21, NAT_D:1, XREAL_1:70;
then ((2 * PI) * ((k * m) mod n)) / n < ((2 * PI) * n) / n by XREAL_1:76;
then A22: ((2 * PI) * ((k * m) mod n)) / n < 2 * PI by XCMPLX_1:90;
A23: 1_ (MultGroup F_Complex) = [**1,0**] by Th20, COMPLFLD:10;
x |^ m = (power F_Complex) . (y,m) by Th32
.= y |^ m by A13, COMPLFLD:112
.= [**(cos (((2 * PI) * (k * m)) / n)),(sin ((((2 * PI) * k) * m) / n))**] by A4, A21, COMPTRIG:71
.= [**(cos (((2 * PI) * ((k * m) mod n)) / n)),(sin (((2 * PI) * ((k * m) mod n)) / n))**] by Th12 ;
then cos (((2 * PI) * ((k * m) mod n)) / n) = 1 by A12, A23, COMPLEX1:163;
hence contradiction by A15, A22, COMPTRIG:21, COMPTRIG:79; :: 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 13;
A24: (((2 * PI) * k) / n) * vn = ((2 * PI) * (kgn * i)) / (n / vn) by A3, XCMPLX_1:83
.= (((2 * PI) * (kgn * i)) * vn) / n by XCMPLX_1:78
.= (((2 * PI) * i) * n) / n by A2
.= ((2 * PI) * i) + 0 by XCMPLX_1:90 ;
x |^ (n div kgn) = (power F_Complex) . (y,vn) by A10, Th32
.= y |^ vn by A8, COMPLFLD:112
.= [**(cos ((((2 * PI) * k) / n) * vn)),(sin ((((2 * PI) * k) / n) * vn))**] by A4, COMPTRIG:71
.= [**(cos 0),(sin (((2 * PI) * i) + 0))**] by A24, COMPLEX2:10
.= 1 + (0 * <i>) by COMPLEX2:9, SIN_COS:34
.= 1_ (MultGroup F_Complex) by Th20, COMPLFLD:10 ;
hence ord x = n div (k gcd n) by A7, A5, A11, GROUP_1:def 12; :: thesis: verum