let n be non zero Element of NAT ; :: thesis:
let x be Element of F_Complex; :: thesis:
assume A1: x in n -roots_of_1 ; :: thesis:

A2: now :: thesis:

assume x = 0. F_Complex ; :: thesis:
then (power F_Complex) . (x,n) <> 1_ F_Complex by VECTSP_1:36;
then x is not CRoot of n, 1_ F_Complex by COMPLFLD:def 2;
hence contradiction by A1, Th21; :: thesis:

end;

then A3: |.x.| > 0 by COMPLFLD:59;
x is CRoot of n, 1_ F_Complex by A1, Th21;
then power (x,n) = 1_ F_Complex by COMPLFLD:def 2;
then A4: 1 = |.x.| to_power n by A2, COMPLFLD:60, POLYNOM5:7;
assume A5: |.x.| <> 1 ; :: thesis:

per cases < 1 or |.x.| > 1 ) by A5, XXREAL_0:1;

suppose A6: |.x.| < 1 ; :: thesis:

reconsider n9 = n as Rational ;
|.x.| #Q n9 < 1 by A3, A6, PREPOWER:65;
hence contradiction by A4, A3, PREPOWER:49; :: thesis:

end;

suppose |.x.| > 1 ; :: thesis:

hence contradiction by A4, POWER:35; :: thesis:

end;

end;