set FC = F_Complex ;

let n be non zero Element of NAT ; :: thesis: for x being Element of (MultGroup F_Complex) holds

( ord x divides n iff x in n -roots_of_1 )

let x be Element of (MultGroup F_Complex); :: thesis: ( ord x divides n iff x in n -roots_of_1 )

reconsider c = x as Element of F_Complex by Th19;

set MGFC = MultGroup F_Complex;

A1: 1_ (MultGroup F_Complex) = 1_ F_Complex by Th17;

then consider c being Element of F_Complex such that

A3: c = x and

A4: c is CRoot of n, 1_ F_Complex ;

(power F_Complex) . (c,n) = 1_ F_Complex by A4, COMPLFLD:def 2;

then x |^ n = 1_ (MultGroup F_Complex) by A1, A3, Th29;

hence ord x divides n by GROUP_1:44; :: thesis: verum

let n be non zero Element of NAT ; :: thesis: for x being Element of (MultGroup F_Complex) holds

( ord x divides n iff x in n -roots_of_1 )

let x be Element of (MultGroup F_Complex); :: thesis: ( ord x divides n iff x in n -roots_of_1 )

reconsider c = x as Element of F_Complex by Th19;

set MGFC = MultGroup F_Complex;

A1: 1_ (MultGroup F_Complex) = 1_ F_Complex by Th17;

hereby :: thesis: ( x in n -roots_of_1 implies ord x divides n )

assume
x in n -roots_of_1
; :: thesis: ord x divides nassume
ord x divides n
; :: thesis: x in n -roots_of_1

then consider k being Nat such that

A2: n = (ord x) * k by NAT_D:def 3;

x |^ (ord x) = 1_ (MultGroup F_Complex) by GROUP_1:41;

then (x |^ (ord x)) |^ k = 1_ (MultGroup F_Complex) by GROUP_1:31;

then x |^ n = 1_ (MultGroup F_Complex) by A2, GROUP_1:35;

then (power F_Complex) . (c,n) = 1_ F_Complex by A1, Th29;

then c is CRoot of n, 1_ F_Complex by COMPLFLD:def 2;

hence x in n -roots_of_1 ; :: thesis: verum

end;then consider k being Nat such that

A2: n = (ord x) * k by NAT_D:def 3;

x |^ (ord x) = 1_ (MultGroup F_Complex) by GROUP_1:41;

then (x |^ (ord x)) |^ k = 1_ (MultGroup F_Complex) by GROUP_1:31;

then x |^ n = 1_ (MultGroup F_Complex) by A2, GROUP_1:35;

then (power F_Complex) . (c,n) = 1_ F_Complex by A1, Th29;

then c is CRoot of n, 1_ F_Complex by COMPLFLD:def 2;

hence x in n -roots_of_1 ; :: thesis: verum

then consider c being Element of F_Complex such that

A3: c = x and

A4: c is CRoot of n, 1_ F_Complex ;

(power F_Complex) . (c,n) = 1_ F_Complex by A4, COMPLFLD:def 2;

then x |^ n = 1_ (MultGroup F_Complex) by A1, A3, Th29;

hence ord x divides n by GROUP_1:44; :: thesis: verum