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;

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

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

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

reconsider y = x as Element of F_Complex by Th19;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;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

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

reconsider i = i as Element of NAT by ORDINAL1:def 12;
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;

end;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

hence
n div kgn <= m
by A6, A9, NAT_D:def 1; :: thesis: verumassume A14:
m < vn
; :: thesis: contradiction

.= (((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;A15: now :: thesis: not (k * m) mod n = 0

A21: (((2 * PI) * k) / n) * m =
((2 * PI) * k) / (n / m)
by XCMPLX_1:82
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;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

.= (((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

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