let n be non empty Element of NAT ; :: thesis:
let k be Element of NAT ; :: thesis:
let x be Element of (MultGroup F_Complex ); :: thesis:
assume A1: x = [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] ; :: thesis:
A2: k gcd n divides n by INT_2:32;
A4: n gcd k > 0 by NEWTON:71;
reconsider kgn = k gcd n as Element of NAT ;
consider vn being Nat such that
A5: n = kgn * vn by A2, NAT_D:def 3;
reconsider vn = vn as Element of NAT by ORDINAL1:def 13;
k gcd n divides k by INT_2:31;
then consider i being Nat such that
A6: k = kgn * i by NAT_D:def 3;
reconsider i = i as Element of NAT by ORDINAL1:def 13;

A7: now

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

end;

A8: n = (kgn * vn) + 0 by A5;
then A9: n div kgn = vn by A4, NAT_D:def 1;
reconsider y = x as Element of F_Complex by Th22;
A10: (((2 * PI ) * k) / n) * vn = ((2 * PI ) * (kgn * i)) / (n / vn) by A6, XCMPLX_1:83
.= (((2 * PI ) * (kgn * i)) * vn) / n by XCMPLX_1:78
.= (((2 * PI ) * i) * n) / n by A5
.= ((2 * PI ) * i) + 0 by XCMPLX_1:90 ;
A11: not vn is empty by A5;
A12: x |^ (n div kgn) = (power F_Complex ) . y,vn by A9, Th32
.= y |^ vn by A11, COMPLFLD:112
.= [**(cos ((((2 * PI ) * k) / n) * vn)),(sin ((((2 * PI ) * k) / n) * vn))**] by A1, COMPTRIG:71
.= [**(cos 0 ),(sin (((2 * PI ) * i) + 0 ))**] by A10, COMPLEX2:10
.= 1 + (0 * <i> ) by COMPLEX2:9, SIN_COS:34
.= 1_ (MultGroup F_Complex ) by Th20, COMPLFLD:10 ;
x in n -roots_of_1 by A1, Th27;
then A13: not x is being_of_order_0 by Th33;
for m being Nat st x |^ m = 1_ (MultGroup F_Complex ) & m <> 0 holds
n div kgn <= m

let m be Nat; :: thesis:
assume that
A14: x |^ m = 1_ (MultGroup F_Complex ) and
A15: m <> 0 ; :: thesis:
reconsider m = m as Element of NAT by ORDINAL1:def 13;

assume A17: m < vn ; :: thesis:

B23: now

assume (k * m) mod n = 0 ; :: thesis:
then A18: n divides k * m by PEPIN:6;
consider a, b being Integer such that
A19: ( k = kgn * a & n = kgn * b ) and
A20: a,b are_relative_prime by INT_2:38;
0 <= b by A19;
then reconsider bi = b as Element of NAT by INT_1:16;
0 <= a by A4, A19;
then reconsider ai = a as Element of NAT by INT_1:16;
A21: m < bi by A4, A9, A17, A19, NAT_D:18;
consider j being Nat such that
A22: k * m = n * j by A18, NAT_D:def 3;
(m * a) * kgn = j * (b * kgn) by A19, A22;
then m * a = ((j * b) * kgn) / kgn by A4, XCMPLX_1:90;
then m * a = j * b by A4, XCMPLX_1:90;
then bi divides m * ai by NAT_D:def 3;
hence contradiction by A15, A20, A21, INT_2:40, NAT_D:7; :: thesis:

end;

A24: (((2 * PI ) * k) / n) * m = ((2 * PI ) * k) / (n / m) by XCMPLX_1:83
.= (((2 * PI ) * k) * m) / n by XCMPLX_1:78 ;
A25: x |^ m = (power F_Complex ) . y,m by Th32
.= y |^ m by A15, COMPLFLD:112
.= [**(cos (((2 * PI ) * (k * m)) / n)),(sin ((((2 * PI ) * k) * m) / n))**] by A1, A24, COMPTRIG:71
.= [**(cos (((2 * PI ) * ((k * m) mod n)) / n)),(sin (((2 * PI ) * ((k * m) mod n)) / n))**] by Th12 ;
1_ (MultGroup F_Complex ) = [**1,0 **] by Th20, COMPLFLD:10;
then A26: cos (((2 * PI ) * ((k * m) mod n)) / n) = 1 by A14, A25, COMPLEX1:163;
B27: (2 * PI ) * 0 < (2 * PI ) * ((k * m) mod n) by B23, COMPTRIG:21;
(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 ((2 * PI ) * ((k * m) mod n)) / n < 2 * PI by XCMPLX_1:90;
hence contradiction by A26, B23, COMPTRIG:21, COMPTRIG:79; :: thesis:

end;

hence n div kgn <= m by A4, A8, NAT_D:def 1; :: thesis:

end;

hence ord x = n div (k gcd n) by A7, A12, A13, GROUP_1:def 12; :: thesis: