let n be non empty Element of NAT ; :: thesis: for x being Element of F_Complex holds
( x in n -roots_of_1 iff ex k being Element of NAT st x = [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] )
let x be Element of F_Complex ; :: thesis: ( x in n -roots_of_1 iff ex k being Element of NAT st x = [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] )

hereby :: thesis: ( ex k being Element of NAT st x = [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] implies x in n -roots_of_1 )

assume A1: x in n -roots_of_1 ; :: thesis: ex k being Element of NAT st x = [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**]

A2: now

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

end;

then A3: ( x = (|.x.| * (cos (Arg x))) + ((|.x.| * (sin (Arg x))) * <i> ) & 0 <= Arg x & Arg x < 2 * PI ) by COMPLFLD:9, COMPTRIG:def 1;
A4: x = [**(|.x.| * (cos (Arg x))),(|.x.| * (sin (Arg x)))**] by A2, COMPLFLD:9, COMPTRIG:def 1;
x is CRoot of n, 1_ F_Complex by A1, Th24;
then (power F_Complex ) . x,n = 1_ F_Complex by COMPLFLD:def 2;
then A5: 1 = |.x.| to_power n by A2, COMPLFLD:97, POLYNOM5:8;

A6: now

assume A7: |.x.| <> 1 ; :: thesis: contradiction
A8: |.x.| > 0 by A2, COMPLFLD:96;

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

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

reconsider n' = n as Rational ;
|.x.| #Q n' < 1 by A8, A9, PREPOWER:76;
hence contradiction by A5, A8, PREPOWER:60; :: thesis: verum

end;

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

hence contradiction by A5, POWER:40; :: thesis: verum

end;

end;

end;

reconsider z = x as Element of COMPLEX by XCMPLX_0:def 2;
A11: z |^ n = ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * <i> ) by COMPTRIG:72;
x is CRoot of n, 1_ F_Complex by A1, Th24;
then (power F_Complex ) . x,n = [**1,0 **] by COMPLFLD:10, COMPLFLD:def 2;
then A12: z |^ n = [**1,0 **] by COMPLFLD:112;
then A13: ( cos (n * (Arg x)) = 1 & sin (n * (Arg x)) = 0 ) by A5, A11, COMPLEX1:163;
consider r being real number such that
A14: ( r = ((2 * PI ) * (- [\((n * (Arg x)) / (2 * PI ))/])) + (n * (Arg x)) & 0 <= r & r < 2 * PI ) by COMPLEX2:2, COMPTRIG:21;
A15: 0 <= (n * (Arg x)) / (2 * PI ) by A3;
set m2 = [\((n * (Arg x)) / (2 * PI ))/];
A16: 0 + (- 1) <= ((n * (Arg x)) / (2 * PI )) + (- 1) by A3, XREAL_1:9;
((n * (Arg x)) / (2 * PI )) - 1 < [\((n * (Arg x)) / (2 * PI ))/] by INT_1:def 4;
then not [\((n * (Arg x)) / (2 * PI ))/] <= - 1 by A16, XXREAL_0:2;
then (- 1) + 1 <= [\((n * (Arg x)) / (2 * PI ))/] by INT_1:20;
then reconsider m = [\((n * (Arg x)) / (2 * PI ))/] as Element of NAT by INT_1:16;
A17: cos (n * (Arg x)) = cos . (((2 * PI ) * m) + r) by A14, SIN_COS:def 23
.= cos . r by SIN_COS2:11
.= cos r by SIN_COS:def 23 ;
sin (n * (Arg x)) = sin . (((2 * PI ) * m) + r) by A14, SIN_COS:def 21
.= sin . r by SIN_COS2:10
.= sin r by SIN_COS:def 21 ;
then ( r = 0 or r = PI ) by A13, A14, COMPTRIG:33;
then (n * (Arg x)) / (n * 1) = ((2 * PI ) * m) / n by A5, A11, A12, A14, A17, COMPLEX1:163, SIN_COS:82;
then ((n / n) * (Arg x)) / 1 = ((2 * PI ) * m) / n by XCMPLX_1:84;
then (Arg x) / 1 = ((2 * PI ) * m) / n by XCMPLX_1:89;
hence ex k being Element of NAT st x = [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] by A4, A6; :: thesis: verum

end;

now

given k being Element of NAT such that A18: x = [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] ; :: thesis: x in n -roots_of_1
set 1F = Arg (1_ F_Complex );
0 + 1 <= n by NAT_1:13;
then A19: n -root 1 = 1 by POWER:7;
reconsider z = 1_ F_Complex as Element of COMPLEX by XCMPLX_0:def 2;
x = ((n -root |.z.|) * (cos (((Arg (1_ F_Complex )) + ((2 * PI ) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg (1_ F_Complex )) + ((2 * PI ) * k)) / n))) * <i> ) by A18, A19, COMPLFLD:10, COMPLFLD:97, COMPTRIG:57;
then x is CRoot of n,z by COMPTRIG:75;
hence x in n -roots_of_1 ; :: thesis: verum

end;

hence ( ex k being Element of NAT st x = [**(cos (((2 * PI ) * k) / n)),(sin (((2 * PI ) * k) / n))**] implies x in n -roots_of_1 ) ; :: thesis: verum