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;
hereby :: thesis: ( x in n -roots_of_1 implies ord x divides n )
assume 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;
assume x in n -roots_of_1 ; :: thesis: ord x divides n
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