let n be non zero Element of NAT ; :: thesis: for x being Element of F_Complex st x in n -roots_of_1 holds
|.x.| = 1
let x be Element of F_Complex; :: thesis: ( x in n -roots_of_1 implies |.x.| = 1 )
assume A1: x in n -roots_of_1 ; :: thesis: |.x.| = 1

A2: now :: thesis: not x = 0. F_Complex

assume x = 0. F_Complex ; :: thesis: contradiction
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: verum

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: contradiction

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

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

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

end;

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

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

end;

end;