set FC = F_Complex ;
let n be non zero Element of NAT ; :: thesis: for x being Element of holds
( ord x divides n iff x in n -roots_of_1 )

let x be Element of ; :: 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_ = 1_ F_Complex by Th17;
hereby :: thesis: ( x in n -roots_of_1 implies ord x divides n )
assume ord x divides n ; :: thesis:
then consider k being Nat such that
A2: n = (ord x) * k by NAT_D:def 3;
x |^ (ord x) = 1_ by GROUP_1:41;
then (x |^ (ord x)) |^ k = 1_ by GROUP_1:31;
then x |^ n = 1_ by ;
then (power F_Complex) . (c,n) = 1_ F_Complex by ;
then c is CRoot of n, 1_ F_Complex by COMPLFLD:def 2;
hence x in n -roots_of_1 ; :: thesis: verum
end;
assume x in n -roots_of_1 ; :: thesis:
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 ;
then x |^ n = 1_ by A1, A3, Th29;
hence ord x divides n by GROUP_1:44; :: thesis: verum