set MGFC = MultGroup F_Complex;
set cMGFC = the carrier of (MultGroup F_Complex);
set FC = F_Complex ;
let n be non zero Element of NAT ; :: thesis: for x being Element of (MultGroup F_Complex) st x in n -roots_of_1 holds
not x is being_of_order_0
let x be Element of the carrier of (MultGroup F_Complex); :: thesis: ( x in n -roots_of_1 implies not x is being_of_order_0 )
assume x in n -roots_of_1 ; :: thesis: not x is being_of_order_0
then consider c being Element of F_Complex such that
A1: c = x and
A2: c is CRoot of n, 1_ F_Complex ;
A3: 1_ (MultGroup F_Complex) = 1_ F_Complex by Th17;
(power F_Complex) . (c,n) = 1_ F_Complex by A2, COMPLFLD:def 2;
then x |^ n = 1_ (MultGroup F_Complex) by A1, A3, Th29;
hence not x is being_of_order_0 ; :: thesis: verum