let z be Complex; :: thesis: exp (- (<i> * z)) = (cos_C /. z) - (<i> * (sin_C /. z))
reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
(cos_C /. z) - (<i> * (sin_C /. z)) = (((exp (<i> * z)) + (exp (- (<i> * z)))) / 2) - (<i> * (sin_C /. z)) by Def2
.= (((exp (<i> * z)) + (exp (- (<i> * z)))) / 2) - (<i> * (((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>))) by Def1
.= ((exp (- (<i> * z))) + (exp (- (<i> * z)))) / 2
.= (((Re (exp (- (<i> * z)))) + (Re (exp (- (<i> * z))))) + (((Im (exp (- (<i> * z)))) + (Im (exp (- (<i> * z))))) * <i>)) / 2 by COMPLEX1:81
.= ((2 * (Re (exp (- (<i> * z))))) + ((2 * (Im (exp (- (<i> * z))))) * <i>)) / 2
.= ((Re (2 * (exp (- (<i> * z))))) + ((2 * (Im (exp (- (<i> * z))))) * <i>)) / 2 by COMSEQ_3:17
.= ((Re (2 * (exp (- (<i> * z))))) + ((Im (2 * (exp (- (<i> * z))))) * <i>)) / 2 by COMSEQ_3:17
.= (2 * (exp (- (<i> * z)))) / 2 by COMPLEX1:13 ;
hence exp (- (<i> * z)) = (cos_C /. z) - (<i> * (sin_C /. z)) ; :: thesis: verum