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

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

hence
ni -roots_of_1 c= n -roots_of_1
; :: thesis: verum
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;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