let n be non zero Element of NAT ; :: thesis: Roots (unital_poly (F_Complex,n)) = n -roots_of_1
now :: thesis: for x being object holds
( ( x in Roots (unital_poly (F_Complex,n)) implies x in n -roots_of_1 ) & ( x in n -roots_of_1 implies x in Roots (unital_poly (F_Complex,n)) ) )
set p = unital_poly (F_Complex,n);
let x be object ; :: thesis: ( ( x in Roots (unital_poly (F_Complex,n)) implies x in n -roots_of_1 ) & ( x in n -roots_of_1 implies x in Roots (unital_poly (F_Complex,n)) ) )
hereby :: thesis: ( x in n -roots_of_1 implies x in Roots (unital_poly (F_Complex,n)) )
assume A1: x in Roots (unital_poly (F_Complex,n)) ; :: thesis: x in n -roots_of_1
then reconsider x9 = x as Element of F_Complex ;
x9 is_a_root_of unital_poly (F_Complex,n) by A1, POLYNOM5:def 10;
then 0. F_Complex = eval ((unital_poly (F_Complex,n)),x9) by POLYNOM5:def 7
.= ((power F_Complex) . (x9,n)) - 1 by Th41 ;
then x9 is CRoot of n, 1_ F_Complex by COMPLFLD:7, COMPLFLD:8, COMPLFLD:def 2;
hence x in n -roots_of_1 ; :: thesis: verum
end;
assume A2: x in n -roots_of_1 ; :: thesis: x in Roots (unital_poly (F_Complex,n))
then reconsider x9 = x as Element of F_Complex ;
x9 is CRoot of n, 1_ F_Complex by A2, Th21;
then (power F_Complex) . (x9,n) = 1 by COMPLFLD:8, COMPLFLD:def 2;
then ((power F_Complex) . (x9,n)) - 1 = 0c ;
then eval ((unital_poly (F_Complex,n)),x9) = 0. F_Complex by Th41, COMPLFLD:7;
then x9 is_a_root_of unital_poly (F_Complex,n) by POLYNOM5:def 7;
hence x in Roots (unital_poly (F_Complex,n)) by POLYNOM5:def 10; :: thesis: verum
end;
hence Roots (unital_poly (F_Complex,n)) = n -roots_of_1 by TARSKI:2; :: thesis: verum