let z1, z2 be Complex; cos_C /. (z1 + z2) = ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. z2))
reconsider z1 = z1, z2 = z2 as Element of COMPLEX by XCMPLX_0:def 2;
set e1 = exp (<i> * z1);
set e2 = exp (- (<i> * z1));
set e3 = exp (<i> * z2);
set e4 = exp (- (<i> * z2));
((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. z2)) =
((cos_C /. z1) * (cos_C /. z2)) - ((((exp (<i> * z1)) - (exp (- (<i> * z1)))) / (2 * <i>)) * (sin_C /. z2))
by Def1
.=
((cos_C /. z1) * (cos_C /. z2)) - ((((exp (<i> * z1)) - (exp (- (<i> * z1)))) / (2 * <i>)) * (((exp (<i> * z2)) - (exp (- (<i> * z2)))) / (2 * <i>)))
by Def1
.=
((cos_C /. z1) * (((exp (<i> * z2)) + (exp (- (<i> * z2)))) / 2)) - ((((exp (<i> * z1)) - (exp (- (<i> * z1)))) / (2 * <i>)) * (((exp (<i> * z2)) - (exp (- (<i> * z2)))) / (2 * <i>)))
by Def2
.=
((((exp (<i> * z1)) + (exp (- (<i> * z1)))) / 2) * (((exp (<i> * z2)) + (exp (- (<i> * z2)))) / 2)) - ((((exp (<i> * z1)) - (exp (- (<i> * z1)))) / (2 * <i>)) * (((exp (<i> * z2)) - (exp (- (<i> * z2)))) / (2 * <i>)))
by Def2
.=
((((exp (<i> * z1)) * (exp (<i> * z2))) + ((exp (<i> * z1)) * (exp (<i> * z2)))) + (((exp (- (<i> * z1))) * (exp (- (<i> * z2)))) + ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) / (2 * 2)
.=
((((Re ((exp (<i> * z1)) * (exp (<i> * z2)))) + (Re ((exp (<i> * z1)) * (exp (<i> * z2))))) + (((Im ((exp (<i> * z1)) * (exp (<i> * z2)))) + (Im ((exp (<i> * z1)) * (exp (<i> * z2))))) * <i>)) + (((exp (- (<i> * z1))) * (exp (- (<i> * z2)))) + ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) / (2 * 2)
by COMPLEX1:81
.=
(((2 * (Re ((exp (<i> * z1)) * (exp (<i> * z2))))) + ((2 * (Im ((exp (<i> * z1)) * (exp (<i> * z2))))) * <i>)) + (((exp (- (<i> * z1))) * (exp (- (<i> * z2)))) + ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) / (2 * 2)
.=
(((Re (2 * ((exp (<i> * z1)) * (exp (<i> * z2))))) + ((2 * (Im ((exp (<i> * z1)) * (exp (<i> * z2))))) * <i>)) + (((exp (- (<i> * z1))) * (exp (- (<i> * z2)))) + ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) / (2 * 2)
by COMSEQ_3:17
.=
(((Re (2 * ((exp (<i> * z1)) * (exp (<i> * z2))))) + ((Im (2 * ((exp (<i> * z1)) * (exp (<i> * z2))))) * <i>)) + (((exp (- (<i> * z1))) * (exp (- (<i> * z2)))) + ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) / (2 * 2)
by COMSEQ_3:17
.=
((2 * ((exp (<i> * z1)) * (exp (<i> * z2)))) + (((exp (- (<i> * z1))) * (exp (- (<i> * z2)))) + ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) / (2 * 2)
by COMPLEX1:13
.=
((2 * ((exp (<i> * z1)) * (exp (<i> * z2)))) + (((Re ((exp (- (<i> * z1))) * (exp (- (<i> * z2))))) + (Re ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) + (((Im ((exp (- (<i> * z1))) * (exp (- (<i> * z2))))) + (Im ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) * <i>))) / (2 * 2)
by COMPLEX1:81
.=
((2 * ((exp (<i> * z1)) * (exp (<i> * z2)))) + ((2 * (Re ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) + ((2 * (Im ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) * <i>))) / (2 * 2)
.=
((2 * ((exp (<i> * z1)) * (exp (<i> * z2)))) + ((Re (2 * ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) + ((2 * (Im ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) * <i>))) / (2 * 2)
by COMSEQ_3:17
.=
((2 * ((exp (<i> * z1)) * (exp (<i> * z2)))) + ((Re (2 * ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) + ((Im (2 * ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) * <i>))) / (2 * 2)
by COMSEQ_3:17
.=
((2 * ((exp (<i> * z1)) * (exp (<i> * z2)))) + (2 * ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) / (2 * 2)
by COMPLEX1:13
.=
(((exp (<i> * z1)) * (exp (<i> * z2))) / 2) + ((2 * ((exp (- (<i> * z1))) * (exp (- (<i> * z2))))) / (2 * 2))
.=
((exp ((<i> * z1) + (<i> * z2))) / 2) + (((exp (- (<i> * z1))) * (exp (- (<i> * z2)))) / 2)
by SIN_COS:23
.=
((exp (<i> * (z1 + z2))) / 2) + ((exp ((- (<i> * z1)) + (- (<i> * z2)))) / 2)
by SIN_COS:23
.=
((exp (<i> * (z1 + z2))) + (exp (- (<i> * (z1 + z2))))) / 2
;
then
cos_C /. (z1 + z2) = ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. z2))
by Def2;
hence
cos_C /. (z1 + z2) = ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. z2))
; verum