let n be non zero 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 :: thesis: not x = 0. F_Complexend;
then ( 0 <= Arg x & Arg x < 2 * PI ) by ;
then A3: 0 + (- 1) <= ((n * (Arg x)) / (2 * PI)) + (- 1) by XREAL_1:7;
x is CRoot of n, 1_ F_Complex by ;
then power (x,n) = 1_ F_Complex by COMPLFLD:def 2;
then A4: 1 = |.x.| to_power n by ;
A5: now :: thesis: not |.x.| <> 1
A6: |.x.| > 0 by ;
assume A7: |.x.| <> 1 ; :: thesis: contradiction
per cases < 1 or |.x.| > 1 ) by ;
suppose A8: |.x.| < 1 ; :: thesis: contradiction
reconsider n9 = n as Rational ;
|.x.| #Q n9 < 1 by ;
hence contradiction by A4, A6, PREPOWER:49; :: thesis: verum
end;
end;
end;
set m2 = [\((n * (Arg x)) / (2 * PI))/];
reconsider z = x as Element of COMPLEX by XCMPLX_0:def 2;
consider r being Real such that
A9: r = ((2 * PI) * (- [\((n * (Arg x)) / (2 * PI))/])) + (n * (Arg x)) and
A10: ( 0 <= r & r < 2 * PI ) by ;
((n * (Arg x)) / (2 * PI)) - 1 < [\((n * (Arg x)) / (2 * PI))/] by INT_1:def 6;
then not [\((n * (Arg x)) / (2 * PI))/] <= - 1 by ;
then (- 1) + 1 <= [\((n * (Arg x)) / (2 * PI))/] by INT_1:7;
then reconsider m = [\((n * (Arg x)) / (2 * PI))/] as Element of NAT by INT_1:3;
A11: cos (n * (Arg x)) = cos . (((2 * PI) * m) + r) by
.= cos . r by SIN_COS2:11
.= cos r by SIN_COS:def 19 ;
A12: sin (n * (Arg x)) = sin . (((2 * PI) * m) + r) by
.= sin . r by SIN_COS2:10
.= sin r by SIN_COS:def 17 ;
x is CRoot of n, 1_ F_Complex by ;
then (power F_Complex) . (x,n) = [**1,0**] by ;
then A13: ( z |^ n = ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * <i>) & z |^ n = [**1,0**] ) by ;
then sin (n * (Arg x)) = 0 by ;
then ( r = 0 or r = PI ) by ;
then (n * (Arg x)) / (n * 1) = ((2 * PI) * m) / n by ;
then ((n / n) * (Arg x)) / 1 = ((2 * PI) * m) / n by XCMPLX_1:83;
then A14: (Arg x) / 1 = ((2 * PI) * m) / n by XCMPLX_1:88;
x = [**(|.x.| * (cos (Arg x))),(|.x.| * (sin (Arg x)))**] by ;
hence ex k being Element of NAT st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] by ; :: thesis: verum
end;
now :: 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 )
reconsider z = 1_ F_Complex as Element of COMPLEX by XCMPLX_0:def 2;
set 1F = Arg ();
given k being Element of NAT such that A15: x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] ; :: thesis:
0 + 1 <= n by NAT_1:13;
then n -root 1 = 1 by POWER:6;
then x = (() * (cos ((() + ((2 * PI) * k)) / n))) + ((() * (sin ((() + ((2 * PI) * k)) / n))) * <i>) by ;
then x is CRoot of n,z by COMPTRIG:57;
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