let z be Element of COMPLEX ; :: thesis: for n being non empty Element of NAT
for k being Element of NAT holds ((n -root |.z.|) * (cos (((Arg z) + ((2 * PI ) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI ) * k)) / n))) * <i> ) is CRoot of n,z
let n be non empty Element of NAT ; :: thesis: for k being Element of NAT holds ((n -root |.z.|) * (cos (((Arg z) + ((2 * PI ) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI ) * k)) / n))) * <i> ) is CRoot of n,z
let k be Element of NAT ; :: thesis: ((n -root |.z.|) * (cos (((Arg z) + ((2 * PI ) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI ) * k)) / n))) * <i> ) is CRoot of n,z
(((n -root |.z.|) * (cos (((Arg z) + ((2 * PI ) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI ) * k)) / n))) * <i> )) |^ n = z by Th56;
hence ((n -root |.z.|) * (cos (((Arg z) + ((2 * PI ) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI ) * k)) / n))) * <i> ) is CRoot of n,z by COMPTRIG:def 2; :: thesis: verum