let n be non zero Element of NAT ; 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 ; 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); ( 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))**]
; 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 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;
( 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
;
n div kgn <= m
reconsider m =
m as
Element of
NAT by ORDINAL1:def 12;
now not m < vnassume A14:
m < vn
;
contradictionA15:
now not (k * m) mod n = 0 assume
(k * m) mod n = 0
;
contradictionthen
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;
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;
verum end;
hence
n div kgn <= m
by A6, A9, NAT_D:def 1;
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; verum