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