let z be Element of COMPLEX ; :: thesis: for n being Element of NAT holds cos_C /. (z + ((2 * n) * PI )) = cos_C /. z
let n be Element of NAT ; :: thesis: cos_C /. (z + ((2 * n) * PI )) = cos_C /. z
cos_C /. (z + ((2 * n) * PI )) = ((exp ((<i> * z) + (<i> * ((2 * n) * PI )))) + (exp (- (<i> * (z + ((2 * n) * PI )))))) / 2 by Def2
.= (((exp (<i> * z)) * (exp (((2 * PI ) * n) * <i> ))) + (exp (- (<i> * (z + ((2 * n) * PI )))))) / 2 by SIN_COS:24
.= (((exp (<i> * z)) * 1) + (exp (- (<i> * (z + ((2 * n) * PI )))))) / 2 by Th28
.= ((exp (<i> * z)) + (exp (((- <i> ) * z) + ((- <i> ) * ((2 * n) * PI ))))) / 2
.= ((exp (<i> * z)) + ((exp ((- <i> ) * z)) * (exp ((- ((2 * PI ) * n)) * <i> )))) / 2 by SIN_COS:24
.= (((exp (<i> * z)) * 1) + ((exp (- (<i> * z))) * 1)) / 2 by Th29
.= ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2 ;
hence cos_C /. (z + ((2 * n) * PI )) = cos_C /. z by Def2; :: thesis: verum