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