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

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

|.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

then A3:
|.x.| > 0
by COMPLFLD:59;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 (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

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;

end;

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;|.x.| #Q n9 < 1 by A3, A6, PREPOWER:65;

hence contradiction by A4, A3, PREPOWER:49; :: thesis: verum