let n be non zero Element of NAT ; :: thesis: for k being Element of NAT holds (cos (((2 * PI) * k) / n)) + ((sin (((2 * PI) * k) / n)) * <i>) is CRoot of n,1
let k be Element of NAT ; :: thesis: (cos (((2 * PI) * k) / n)) + ((sin (((2 * PI) * k) / n)) * <i>) is CRoot of n,1
((cos (((2 * PI) * k) / n)) + ((sin (((2 * PI) * k) / n)) * <i>)) |^ n = (cos (n * (((2 * PI) * k) / n))) + ((sin (n * (((2 * PI) * k) / n))) * <i>) by Th31
.= (cos ((2 * PI) * k)) + ((sin (n * (((2 * PI) * k) / n))) * <i>) by XCMPLX_1:87
.= (cos (((2 * PI) * k) + 0)) + ((sin (((2 * PI) * k) + 0)) * <i>) by XCMPLX_1:87
.= (cos . (((2 * PI) * k) + 0)) + ((sin (((2 * PI) * k) + 0)) * <i>) by SIN_COS:def 19
.= (cos . (((2 * PI) * k) + 0)) + ((sin . (((2 * PI) * k) + 0)) * <i>) by SIN_COS:def 17
.= (cos . (((2 * PI) * k) + 0)) + ((sin . 0) * <i>) by SIN_COS2:10
.= 1 by SIN_COS:30, SIN_COS2:11 ;
hence (cos (((2 * PI) * k) / n)) + ((sin (((2 * PI) * k) / n)) * <i>) is CRoot of n,1 by COMPTRIG:def 2; :: thesis: verum