let n be non zero Element of NAT ; :: thesis: for x, y being Element of COMPLEX st x in n -roots_of_1 & y in n -roots_of_1 holds

x * y in n -roots_of_1

let x, y be Element of COMPLEX ; :: thesis: ( x in n -roots_of_1 & y in n -roots_of_1 implies x * y in n -roots_of_1 )

assume that

A1: x in n -roots_of_1 and

A2: y in n -roots_of_1 ; :: thesis: x * y in n -roots_of_1

reconsider a = x as Element of F_Complex by COMPLFLD:def 1;

consider i being Element of NAT such that

A3: a = [**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] by A1, Th24;

reconsider b = y as Element of F_Complex by COMPLFLD:def 1;

consider j being Element of NAT such that

A4: b = [**(cos (((2 * PI) * j) / n)),(sin (((2 * PI) * j) / n))**] by A2, Th24;

a * b = [**(cos (((2 * PI) * ((i + j) mod n)) / n)),(sin (((2 * PI) * ((i + j) mod n)) / n))**] by A3, A4, Th11;

hence x * y in n -roots_of_1 by Th24; :: thesis: verum

x * y in n -roots_of_1

let x, y be Element of COMPLEX ; :: thesis: ( x in n -roots_of_1 & y in n -roots_of_1 implies x * y in n -roots_of_1 )

assume that

A1: x in n -roots_of_1 and

A2: y in n -roots_of_1 ; :: thesis: x * y in n -roots_of_1

reconsider a = x as Element of F_Complex by COMPLFLD:def 1;

consider i being Element of NAT such that

A3: a = [**(cos (((2 * PI) * i) / n)),(sin (((2 * PI) * i) / n))**] by A1, Th24;

reconsider b = y as Element of F_Complex by COMPLFLD:def 1;

consider j being Element of NAT such that

A4: b = [**(cos (((2 * PI) * j) / n)),(sin (((2 * PI) * j) / n))**] by A2, Th24;

a * b = [**(cos (((2 * PI) * ((i + j) mod n)) / n)),(sin (((2 * PI) * ((i + j) mod n)) / n))**] by A3, A4, Th11;

hence x * y in n -roots_of_1 by Th24; :: thesis: verum