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 n
let z be Element of COMPLEX ; :: thesis: exp (- ((<i> * n) * z)) = ((cos_C /. z) - (<i> * (sin_C /. z))) #N 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 n by Th52; :: thesis: verum