let z1, z2 be complex number ; sin_C /. (z1 + z2) = ((sin_C /. z1) * (cos_C /. z2)) + ((cos_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));
((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2)) =
((((exp (<i> * z1)) - (exp (- (<i> * z1)))) / (2 * <i>)) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2))
by Def1
.=
((((exp (<i> * z1)) - (exp (- (<i> * z1)))) / (2 * <i>)) * (cos_C /. z2)) + ((cos_C /. z1) * (((exp (<i> * z2)) - (exp (- (<i> * z2)))) / (2 * <i>)))
by Def1
.=
((((exp (<i> * z1)) - (exp (- (<i> * z1)))) / (2 * <i>)) * (((exp (- (<i> * z2))) + (exp (<i> * z2))) / 2)) + ((cos_C /. z1) * (((exp (<i> * z2)) - (exp (- (<i> * z2)))) / (2 * <i>)))
by Def2
.=
((((exp (<i> * z1)) - (exp (- (<i> * z1)))) * ((exp (- (<i> * z2))) + (exp (<i> * z2)))) / ((2 * <i>) * 2)) + ((((exp (- (<i> * z1))) + (exp (<i> * z1))) / 2) * (((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))))) - (((exp (<i> * z1)) * (exp (- (<i> * z2)))) - ((exp (- (<i> * z1))) * (exp (- (<i> * z2))))))) / ((2 * <i>) * 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 * <i>) * 2)
by COMPLEX1:def 5
.=
(((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 * <i>) * 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 * <i>) * 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 * <i>) * 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 * <i>) * 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 * <i>) * 2)
by COMPLEX1:def 5
.=
((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 * <i>) * 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 * <i>) * 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 * <i>) * 2)
by COMSEQ_3:17
.=
((2 * ((exp (<i> * z1)) * (exp (<i> * z2)))) - (2 * ((exp (- (<i> * z1))) * (exp (- (<i> * z2)))))) / ((2 * <i>) * 2)
by COMPLEX1:13
.=
(((exp (<i> * z1)) * (exp (<i> * z2))) / (2 * <i>)) - ((2 * ((exp (- (<i> * z1))) * (exp (- (<i> * z2))))) / ((2 * <i>) * 2))
.=
((exp ((<i> * z1) + (<i> * z2))) / (2 * <i>)) - (((exp (- (<i> * z1))) * (exp (- (<i> * z2)))) / (2 * <i>))
by SIN_COS:23
.=
((exp (<i> * (z1 + z2))) / (2 * <i>)) - ((exp ((- (<i> * z1)) + (- (<i> * z2)))) / (2 * <i>))
by SIN_COS:23
.=
((exp (<i> * (z1 + z2))) - (exp (- (<i> * (z1 + z2))))) / (2 * <i>)
;
then
sin_C /. (z1 + z2) = ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2))
by Def1;
hence
sin_C /. (z1 + z2) = ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2))
; verum