set cMGFC = the carrier of ;
set MGFC = MultGroup F_Complex;
let n be non zero Element of NAT ; :: thesis: n -roots_of_1 = { x where x is Element of : ord x divides n }
set R = { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ;
set S = { x where x is Element of : ord x divides n } ;
A1: n -roots_of_1 = { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ;
then A2: { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } c= the carrier of by Th32;
now :: thesis: for a being object holds
( ( a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } implies a in { x where x is Element of : ord x divides n } ) & ( a in { x where x is Element of : ord x divides n } implies a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ) )
let a be object ; :: thesis: ( ( a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } implies a in { x where x is Element of : ord x divides n } ) & ( a in { x where x is Element of : ord x divides n } implies a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ) )
hereby :: thesis: ( a in { x where x is Element of : ord x divides n } implies a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } )
assume A3: a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } ; :: thesis: a in { x where x is Element of : ord x divides n }
then reconsider x = a as Element of by A2;
ord x divides n by A1, A3, Th34;
hence a in { x where x is Element of : ord x divides n } ; :: thesis: verum
end;
assume a in { x where x is Element of : ord x divides n } ; :: thesis: a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex }
then ex x being Element of st
( a = x & ord x divides n ) ;
hence a in { a where a is Element of F_Complex : a is CRoot of n, 1_ F_Complex } by ; :: thesis: verum
end;
hence n -roots_of_1 = { x where x is Element of : ord x divides n } by TARSKI:2; :: thesis: verum