let n, ni be non zero Element of NAT ; :: thesis: ( ni divides n implies ni -roots_of_1 c= n -roots_of_1 )
assume ni divides n ; :: thesis: ni -roots_of_1 c= n -roots_of_1
then consider k being Nat such that
A1: n = ni * k by NAT_D:def 3;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
for x being object st x in ni -roots_of_1 holds
x in n -roots_of_1
proof
let x be object ; :: thesis: ( x in ni -roots_of_1 implies x in n -roots_of_1 )
assume A2: x in ni -roots_of_1 ; :: thesis: x in n -roots_of_1
reconsider y = x as Element of F_Complex by A2;
y is CRoot of ni, 1_ F_Complex by A2, Th21;
then 1_ F_Complex = (power F_Complex) . (y,ni) by COMPLFLD:def 2;
then 1_ F_Complex = (power F_Complex) . (((power F_Complex) . (y,ni)),k) by Th8;
then 1_ F_Complex = (power F_Complex) . (y,n) by A1, Th12;
then y is CRoot of n, 1_ F_Complex by COMPLFLD:def 2;
hence x in n -roots_of_1 ; :: thesis: verum
end;
hence ni -roots_of_1 c= n -roots_of_1 ; :: thesis: verum