let n be Element of NAT ; :: thesis: for z being Element of COMPLEX holds exp (- ((<i> * n) * z)) = ((cos_C /. z) - (<i> * (sin_C /. z))) |^ n
let z be Element of COMPLEX ; :: thesis: exp (- ((<i> * n) * z)) = ((cos_C /. z) - (<i> * (sin_C /. z))) |^ n
exp (- ((<i> * n) * z)) = exp (- (<i> * (n * z)))
.= (cos_C /. (n * z)) - (<i> * (sin_C /. (n * z))) by Th37 ;
hence exp (- ((<i> * n) * z)) = ((cos_C /. z) - (<i> * (sin_C /. z))) |^ n by Th51; :: thesis: verum