let n be non zero Element of NAT ; :: thesis: card (n -roots_of_1) = n

set X = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ;

defpred S_{1}[ object , object ] means ex j being Element of NAT st

( j = $1 & $2 = [**(cos (((2 * PI) * (j -' 1)) / n)),(sin (((2 * PI) * (j -' 1)) / n))**] );

A1: { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } = n -roots_of_1 by Th26;

[**(cos (((2 * PI) * 0) / n)),(sin (((2 * PI) * 0) / n))**] in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ;

then reconsider Y = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } as non empty set ;

A2: for x being object st x in Seg n holds

ex y being object st

( y in Y & S_{1}[x,y] )

A6: for x being object st x in Seg n holds

S_{1}[x,F . x]
from FUNCT_2:sch 1(A2);

for c being object st c in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } holds

ex x being object st

( x in Seg n & c = F . x )

A12: dom F = Seg n by FUNCT_2:def 1;

for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds

x1 = x2

then Seg n,F .: (Seg n) are_equipotent by A12, CARD_1:33;

then Seg n, rng F are_equipotent by A12, RELAT_1:113;

then card (Seg n) = card { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } by A11, CARD_1:5;

hence card (n -roots_of_1) = n by A1, FINSEQ_1:57; :: thesis: verum

set X = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ;

defpred S

( j = $1 & $2 = [**(cos (((2 * PI) * (j -' 1)) / n)),(sin (((2 * PI) * (j -' 1)) / n))**] );

A1: { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } = n -roots_of_1 by Th26;

[**(cos (((2 * PI) * 0) / n)),(sin (((2 * PI) * 0) / n))**] in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ;

then reconsider Y = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } as non empty set ;

A2: for x being object st x in Seg n holds

ex y being object st

( y in Y & S

proof

consider F being Function of (Seg n),Y such that
let x be object ; :: thesis: ( x in Seg n implies ex y being object st

( y in Y & S_{1}[x,y] ) )

assume A3: x in Seg n ; :: thesis: ex y being object st

( y in Y & S_{1}[x,y] )

reconsider a = x as Element of NAT by A3;

a <= n by A3, FINSEQ_1:1;

then a < n + 1 by NAT_1:13;

then A4: a - 1 < (n + 1) - 1 by XREAL_1:14;

consider b being Element of NAT such that

A5: b = a -' 1 ;

1 <= a by A3, FINSEQ_1:1;

then a -' 1 < n by A4, XREAL_1:233;

then [**(cos (((2 * PI) * b) / n)),(sin (((2 * PI) * b) / n))**] in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } by A5;

hence ex y being object st

( y in Y & S_{1}[x,y] )
by A5; :: thesis: verum

end;( y in Y & S

assume A3: x in Seg n ; :: thesis: ex y being object st

( y in Y & S

reconsider a = x as Element of NAT by A3;

a <= n by A3, FINSEQ_1:1;

then a < n + 1 by NAT_1:13;

then A4: a - 1 < (n + 1) - 1 by XREAL_1:14;

consider b being Element of NAT such that

A5: b = a -' 1 ;

1 <= a by A3, FINSEQ_1:1;

then a -' 1 < n by A4, XREAL_1:233;

then [**(cos (((2 * PI) * b) / n)),(sin (((2 * PI) * b) / n))**] in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } by A5;

hence ex y being object st

( y in Y & S

A6: for x being object st x in Seg n holds

S

for c being object st c in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } holds

ex x being object st

( x in Seg n & c = F . x )

proof

then A11:
rng F = { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n }
by FUNCT_2:10;
let c be object ; :: thesis: ( c in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } implies ex x being object st

( x in Seg n & c = F . x ) )

assume c in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ; :: thesis: ex x being object st

( x in Seg n & c = F . x )

then consider k being Element of NAT such that

A7: c = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] and

A8: k < n ;

A9: (k + 1) -' 1 = k by NAT_D:34;

( 0 + 1 <= k + 1 & k + 1 <= n ) by A8, INT_1:7;

then A10: k + 1 in Seg n by FINSEQ_1:1;

then ex j being Element of NAT st

( j = k + 1 & F . (k + 1) = [**(cos (((2 * PI) * (j -' 1)) / n)),(sin (((2 * PI) * (j -' 1)) / n))**] ) by A6;

hence ex x being object st

( x in Seg n & c = F . x ) by A7, A10, A9; :: thesis: verum

end;( x in Seg n & c = F . x ) )

assume c in { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } ; :: thesis: ex x being object st

( x in Seg n & c = F . x )

then consider k being Element of NAT such that

A7: c = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] and

A8: k < n ;

A9: (k + 1) -' 1 = k by NAT_D:34;

( 0 + 1 <= k + 1 & k + 1 <= n ) by A8, INT_1:7;

then A10: k + 1 in Seg n by FINSEQ_1:1;

then ex j being Element of NAT st

( j = k + 1 & F . (k + 1) = [**(cos (((2 * PI) * (j -' 1)) / n)),(sin (((2 * PI) * (j -' 1)) / n))**] ) by A6;

hence ex x being object st

( x in Seg n & c = F . x ) by A7, A10, A9; :: thesis: verum

A12: dom F = Seg n by FUNCT_2:def 1;

for x1, x2 being object st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds

x1 = x2

proof

then
F is one-to-one
by FUNCT_1:def 4;
let x1, x2 be object ; :: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )

assume that

A13: x1 in dom F and

A14: x2 in dom F and

A15: F . x1 = F . x2 ; :: thesis: x1 = x2

A16: x1 in Seg n by A13, FUNCT_2:def 1;

then consider j being Element of NAT such that

A17: j = x1 and

A18: F . x1 = [**(cos (((2 * PI) * (j -' 1)) / n)),(sin (((2 * PI) * (j -' 1)) / n))**] by A6;

set a1 = ((2 * PI) * (j -' 1)) / n;

A19: 1 <= j by A16, A17, FINSEQ_1:1;

j <= n by A16, A17, FINSEQ_1:1;

then j - 1 < n by XREAL_1:146, XXREAL_0:2;

then j -' 1 < n by A19, XREAL_1:233;

then (j -' 1) / n < n / n by XREAL_1:74;

then (j -' 1) / n < 1 by XCMPLX_1:60;

then ((j -' 1) / n) * (2 * PI) < 1 * (2 * PI) by COMPTRIG:5, XREAL_1:68;

then A20: ((2 * PI) * (j -' 1)) / n < 2 * PI by XCMPLX_1:74;

A21: x2 in Seg n by A14, FUNCT_2:def 1;

then consider k being Element of NAT such that

A22: k = x2 and

A23: F . x2 = [**(cos (((2 * PI) * (k -' 1)) / n)),(sin (((2 * PI) * (k -' 1)) / n))**] by A6;

set a2 = ((2 * PI) * (k -' 1)) / n;

A24: 1 <= k by A21, A22, FINSEQ_1:1;

k <= n by A21, A22, FINSEQ_1:1;

then k - 1 < n by XREAL_1:146, XXREAL_0:2;

then k -' 1 < n by A24, XREAL_1:233;

then (k -' 1) / n < n / n by XREAL_1:74;

then (k -' 1) / n < 1 by XCMPLX_1:60;

then ((k -' 1) / n) * (2 * PI) < 1 * (2 * PI) by COMPTRIG:5, XREAL_1:68;

then A25: ((2 * PI) * (k -' 1)) / n < 2 * PI by XCMPLX_1:74;

cos (((2 * PI) * (j -' 1)) / n) = cos (((2 * PI) * (k -' 1)) / n) by A15, A18, A23, COMPLEX1:77;

then ((2 * PI) * (j -' 1)) / n = ((2 * PI) * (k -' 1)) / n by A15, A18, A23, A20, A25, COMPLEX2:11, COMPTRIG:5;

then (((2 * PI) * (j -' 1)) / n) * n = (2 * PI) * (k -' 1) by XCMPLX_1:87;

then j -' 1 = k -' 1 by COMPTRIG:5, XCMPLX_1:5, XCMPLX_1:87;

then j = (k -' 1) + 1 by A19, XREAL_1:235;

hence x1 = x2 by A17, A22, A24, XREAL_1:235; :: thesis: verum

end;assume that

A13: x1 in dom F and

A14: x2 in dom F and

A15: F . x1 = F . x2 ; :: thesis: x1 = x2

A16: x1 in Seg n by A13, FUNCT_2:def 1;

then consider j being Element of NAT such that

A17: j = x1 and

A18: F . x1 = [**(cos (((2 * PI) * (j -' 1)) / n)),(sin (((2 * PI) * (j -' 1)) / n))**] by A6;

set a1 = ((2 * PI) * (j -' 1)) / n;

A19: 1 <= j by A16, A17, FINSEQ_1:1;

j <= n by A16, A17, FINSEQ_1:1;

then j - 1 < n by XREAL_1:146, XXREAL_0:2;

then j -' 1 < n by A19, XREAL_1:233;

then (j -' 1) / n < n / n by XREAL_1:74;

then (j -' 1) / n < 1 by XCMPLX_1:60;

then ((j -' 1) / n) * (2 * PI) < 1 * (2 * PI) by COMPTRIG:5, XREAL_1:68;

then A20: ((2 * PI) * (j -' 1)) / n < 2 * PI by XCMPLX_1:74;

A21: x2 in Seg n by A14, FUNCT_2:def 1;

then consider k being Element of NAT such that

A22: k = x2 and

A23: F . x2 = [**(cos (((2 * PI) * (k -' 1)) / n)),(sin (((2 * PI) * (k -' 1)) / n))**] by A6;

set a2 = ((2 * PI) * (k -' 1)) / n;

A24: 1 <= k by A21, A22, FINSEQ_1:1;

k <= n by A21, A22, FINSEQ_1:1;

then k - 1 < n by XREAL_1:146, XXREAL_0:2;

then k -' 1 < n by A24, XREAL_1:233;

then (k -' 1) / n < n / n by XREAL_1:74;

then (k -' 1) / n < 1 by XCMPLX_1:60;

then ((k -' 1) / n) * (2 * PI) < 1 * (2 * PI) by COMPTRIG:5, XREAL_1:68;

then A25: ((2 * PI) * (k -' 1)) / n < 2 * PI by XCMPLX_1:74;

cos (((2 * PI) * (j -' 1)) / n) = cos (((2 * PI) * (k -' 1)) / n) by A15, A18, A23, COMPLEX1:77;

then ((2 * PI) * (j -' 1)) / n = ((2 * PI) * (k -' 1)) / n by A15, A18, A23, A20, A25, COMPLEX2:11, COMPTRIG:5;

then (((2 * PI) * (j -' 1)) / n) * n = (2 * PI) * (k -' 1) by XCMPLX_1:87;

then j -' 1 = k -' 1 by COMPTRIG:5, XCMPLX_1:5, XCMPLX_1:87;

then j = (k -' 1) + 1 by A19, XREAL_1:235;

hence x1 = x2 by A17, A22, A24, XREAL_1:235; :: thesis: verum

then Seg n,F .: (Seg n) are_equipotent by A12, CARD_1:33;

then Seg n, rng F are_equipotent by A12, RELAT_1:113;

then card (Seg n) = card { [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] where k is Element of NAT : k < n } by A11, CARD_1:5;

hence card (n -roots_of_1) = n by A1, FINSEQ_1:57; :: thesis: verum