let z1, z2 be Complex; cosh_C /. (z1 - z2) = ((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. z2))
set e1 = exp z1;
set e2 = exp (- z1);
set e3 = exp z2;
set e4 = exp (- z2);
((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. z2)) =
((((exp z1) + (exp (- z1))) / 2) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. z2))
by Def4
.=
((((exp z1) + (exp (- z1))) / 2) * (((exp z2) + (exp (- z2))) / 2)) - ((sinh_C /. z1) * (sinh_C /. z2))
by Def4
.=
((((exp z1) + (exp (- z1))) * ((exp z2) + (exp (- z2)))) / (2 * 2)) - ((((exp z1) - (exp (- z1))) / 2) * (sinh_C /. z2))
by Def3
.=
((((exp z1) + (exp (- z1))) * ((exp z2) + (exp (- z2)))) / (2 * 2)) - ((((exp z1) - (exp (- z1))) / 2) * (((exp z2) - (exp (- z2))) / 2))
by Def3
.=
((((exp (- z1)) * (exp z2)) + ((exp (- z1)) * (exp z2))) + ((((exp z1) * (exp (- z2))) + ((exp (- z1)) * (exp (- z2)))) + (((exp z1) * (exp (- z2))) - ((exp (- z1)) * (exp (- z2)))))) / (2 * 2)
.=
((((Re ((exp (- z1)) * (exp z2))) + (Re ((exp (- z1)) * (exp z2)))) + (((Im ((exp (- z1)) * (exp z2))) + (Im ((exp (- z1)) * (exp z2)))) * <i>)) + (((exp z1) * (exp (- z2))) + ((exp z1) * (exp (- z2))))) / (2 * 2)
by COMPLEX1:81
.=
(((2 * (Re ((exp (- z1)) * (exp z2)))) + ((2 * (Im ((exp (- z1)) * (exp z2)))) * <i>)) + (((exp z1) * (exp (- z2))) + ((exp z1) * (exp (- z2))))) / (2 * 2)
.=
(((Re (2 * ((exp (- z1)) * (exp z2)))) + ((2 * (Im ((exp (- z1)) * (exp z2)))) * <i>)) + (((exp z1) * (exp (- z2))) + ((exp z1) * (exp (- z2))))) / (2 * 2)
by COMSEQ_3:17
.=
(((Re (2 * ((exp (- z1)) * (exp z2)))) + ((Im (2 * ((exp (- z1)) * (exp z2)))) * <i>)) + (((exp z1) * (exp (- z2))) + ((exp z1) * (exp (- z2))))) / (2 * 2)
by COMSEQ_3:17
.=
((2 * ((exp (- z1)) * (exp z2))) + (((exp z1) * (exp (- z2))) + ((exp z1) * (exp (- z2))))) / (2 * 2)
by COMPLEX1:13
.=
((2 * ((exp (- z1)) * (exp z2))) + (((Re ((exp z1) * (exp (- z2)))) + (Re ((exp z1) * (exp (- z2))))) + (((Im ((exp z1) * (exp (- z2)))) + (Im ((exp z1) * (exp (- z2))))) * <i>))) / (2 * 2)
by COMPLEX1:81
.=
((2 * ((exp (- z1)) * (exp z2))) + ((2 * (Re ((exp z1) * (exp (- z2))))) + ((2 * (Im ((exp z1) * (exp (- z2))))) * <i>))) / (2 * 2)
.=
((2 * ((exp (- z1)) * (exp z2))) + ((Re (2 * ((exp z1) * (exp (- z2))))) + ((2 * (Im ((exp z1) * (exp (- z2))))) * <i>))) / (2 * 2)
by COMSEQ_3:17
.=
((2 * ((exp (- z1)) * (exp z2))) + ((Re (2 * ((exp z1) * (exp (- z2))))) + ((Im (2 * ((exp z1) * (exp (- z2))))) * <i>))) / (2 * 2)
by COMSEQ_3:17
.=
((2 * ((exp (- z1)) * (exp z2))) + (2 * ((exp z1) * (exp (- z2))))) / (2 * 2)
by COMPLEX1:13
.=
(((exp z1) * (exp (- z2))) / 2) + ((2 * ((exp (- z1)) * (exp z2))) / (2 * 2))
.=
((exp (z1 + (- z2))) / 2) + (((exp (- z1)) * (exp z2)) / 2)
by SIN_COS:23
.=
((exp (z1 - z2)) / 2) + ((exp ((- z1) + z2)) / 2)
by SIN_COS:23
.=
((exp (z1 - z2)) + (exp (- (z1 - z2)))) / 2
;
hence
cosh_C /. (z1 - z2) = ((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. z2))
by Def4; verum