let n be Element of NAT ; :: thesis: for z being Element of COMPLEX holds ((cos_C /. z) - (<i> * (sin_C /. z))) #N n = (cos_C /. (n * z)) - (<i> * (sin_C /. (n * z)))
let z be Element of COMPLEX ; :: thesis: ((cos_C /. z) - (<i> * (sin_C /. z))) #N n = (cos_C /. (n * z)) - (<i> * (sin_C /. (n * z)))
((cos_C /. z) - (<i> * (sin_C /. z))) #N n = ((cos_C /. z) + (<i> * (- (sin_C /. z)))) #N n
.= ((cos_C /. z) + (<i> * (sin_C /. (- z)))) #N n by Th2
.= ((cos_C /. (- z)) + (<i> * (sin_C /. (- z)))) #N n by Th3
.= (cos_C /. (- (n * z))) + (<i> * (sin_C /. (n * (- z)))) by Th51
.= (cos_C /. (n * z)) + (<i> * (sin_C /. (- (n * z)))) by Th3
.= (cos_C /. (n * z)) + (<i> * (- (sin_C /. (n * z)))) by Th2
.= (cos_C /. (n * z)) + (- (<i> * (sin_C /. (n * z)))) ;
hence ((cos_C /. z) - (<i> * (sin_C /. z))) #N n = (cos_C /. (n * z)) - (<i> * (sin_C /. (n * z))) ; :: thesis: verum