let x be Real; :: thesis: for n, k being Nat st n <> 0 holds
((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * <i>)) |^ n = (cos x) + ((sin x) * <i>)
let n, k be Nat; :: thesis: ( n <> 0 implies ((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * <i>)) |^ n = (cos x) + ((sin x) * <i>) )
assume A1: n <> 0 ; :: thesis: ((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * <i>)) |^ n = (cos x) + ((sin x) * <i>)
thus ((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * <i>)) |^ n = (cos (n * ((x + ((2 * PI) * k)) / n))) + ((sin (n * ((x + ((2 * PI) * k)) / n))) * <i>) by Th53
.= (cos (x + ((2 * PI) * k))) + ((sin (n * ((x + ((2 * PI) * k)) / n))) * <i>) by A1, XCMPLX_1:87
.= (cos (x + ((2 * PI) * k))) + ((sin (x + ((2 * PI) * k))) * <i>) by A1, XCMPLX_1:87
.= (cos . (x + ((2 * PI) * k))) + ((sin (x + ((2 * PI) * k))) * <i>) by SIN_COS:def 19
.= (cos . (x + ((2 * PI) * k))) + ((sin . (x + ((2 * PI) * k))) * <i>) by SIN_COS:def 17
.= (cos . (x + ((2 * PI) * k))) + ((sin . x) * <i>) by SIN_COS2:10
.= (cos . x) + ((sin . x) * <i>) by SIN_COS2:11
.= (cos . x) + ((sin x) * <i>) by SIN_COS:def 17
.= (cos x) + ((sin x) * <i>) by SIN_COS:def 19 ; :: thesis: verum