let n be Element of NAT ; :: thesis: for z being Complex holds ((cos_C /. z) - (<i> * (sin_C /. z))) |^ n = (cos_C /. (n * z)) - (<i> * (sin_C /. (n * z)))
let z be Complex; :: thesis: ((cos_C /. z) - (<i> * (sin_C /. z))) |^ n = (cos_C /. (n * z)) - (<i> * (sin_C /. (n * z)))
((cos_C /. z) - (<i> * (sin_C /. z))) |^ n = ((cos_C /. z) + (<i> * (- (sin_C /. z)))) |^ n
.= ((cos_C /. z) + (<i> * (sin_C /. (- z)))) |^ n by Th2
.= ((cos_C /. (- z)) + (<i> * (sin_C /. (- z)))) |^ n by Th3
.= (cos_C /. (- (n * z))) + (<i> * (sin_C /. (n * (- z)))) by Th50
.= (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 = (cos_C /. (n * z)) - (<i> * (sin_C /. (n * z))) ; :: thesis: verum