theorem Th55: :: COMPTRIG:55

for x being Real
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>)