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_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 ( 0 <= Arg x & Arg x < 2 * PI ) by COMPLFLD:7, COMPTRIG:def 1;
then A3: 0 + (- 1) <= ((n * (Arg x)) / (2 * PI)) + (- 1) by XREAL_1:7;
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;
A5: now :: thesis: not |.x.| <> 1
A6: |.x.| > 0 by A2, COMPLFLD:59;
assume A7: |.x.| <> 1 ; :: thesis: contradiction
per cases ( |.x.| < 1 or |.x.| > 1 ) by A7, XXREAL_0:1;
suppose A8: |.x.| < 1 ; :: thesis: contradiction
reconsider n9 = n as Rational ;
|.x.| #Q n9 < 1 by A6, A8, PREPOWER:65;
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 COMPLEX2:1, COMPTRIG:5;
((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 A3, XXREAL_0:2;
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 A9, SIN_COS:def 19
.= cos . r by SIN_COS2:11
.= cos r by SIN_COS:def 19 ;
A12: sin (n * (Arg x)) = sin . (((2 * PI) * m) + r) by A9, SIN_COS:def 17
.= sin . r by SIN_COS2:10
.= sin r by SIN_COS:def 17 ;
x is CRoot of n, 1_ F_Complex by A1, Th21;
then (power F_Complex) . (x,n) = [**1,0**] by COMPLFLD:8, COMPLFLD:def 2;
then A13: ( z |^ n = ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * <i>) & z |^ n = [**1,0**] ) by COMPLFLD:74, COMPTRIG:54;
then sin (n * (Arg x)) = 0 by A4, COMPLEX1:77;
then ( r = 0 or r = PI ) by A10, A12, COMPTRIG:17;
then (n * (Arg x)) / (n * 1) = ((2 * PI) * m) / n by A4, A13, A9, A11, COMPLEX1:77, SIN_COS:77;
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 A2, COMPLFLD:7, COMPTRIG:def 1;
hence ex k being Element of NAT st x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] by A5, A14; :: 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 (1_ F_Complex);
given k being Element of NAT such that A15: x = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] ; :: thesis: x in n -roots_of_1
0 + 1 <= n by NAT_1:13;
then n -root 1 = 1 by POWER:6;
then 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 A15, COMPLFLD:8, COMPLFLD:60, COMPTRIG:39;
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