let n be non empty 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 Th53
.= (cos ((2 * PI ) * k)) + ((sin (n * (((2 * PI ) * k) / n))) * <i> ) by XCMPLX_1:88
.= (cos (((2 * PI ) * k) + 0 )) + ((sin (((2 * PI ) * k) + 0 )) * <i> ) by XCMPLX_1:88
.= (cos . (((2 * PI ) * k) + 0 )) + ((sin (((2 * PI ) * k) + 0 )) * <i> ) by SIN_COS:def 23
.= (cos . (((2 * PI ) * k) + 0 )) + ((sin . (((2 * PI ) * k) + 0 )) * <i> ) by SIN_COS:def 21
.= (cos . (((2 * PI ) * k) + 0 )) + ((sin . 0 ) * <i> ) by SIN_COS2:10
.= 1 by SIN_COS:33, 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