let y, z be Real; ( cosh (y + z) = ((cosh y) * (cosh z)) + ((sinh y) * (sinh z)) & cosh (y - z) = ((cosh y) * (cosh z)) - ((sinh y) * (sinh z)) & sinh (y + z) = ((sinh y) * (cosh z)) + ((cosh y) * (sinh z)) & sinh (y - z) = ((sinh y) * (cosh z)) - ((cosh y) * (sinh z)) & tanh (y + z) = ((tanh y) + (tanh z)) / (1 + ((tanh y) * (tanh z))) & tanh (y - z) = ((tanh y) - (tanh z)) / (1 - ((tanh y) * (tanh z))) )
A1: ((cosh y) * (cosh z)) - ((sinh y) * (sinh z)) =
((cosh . y) * (cosh z)) - ((sinh y) * (sinh z))
by SIN_COS2:def 4
.=
((cosh . y) * (cosh . z)) - ((sinh y) * (sinh z))
by SIN_COS2:def 4
.=
((cosh . y) * (cosh . z)) - ((sinh . y) * (sinh z))
by SIN_COS2:def 2
.=
((cosh . y) * (cosh . z)) - ((sinh . y) * (sinh . z))
by SIN_COS2:def 2
.=
cosh . (y - z)
by SIN_COS2:20
.=
cosh (y - z)
by SIN_COS2:def 4
;
A2: ((sinh y) * (cosh z)) + ((cosh y) * (sinh z)) =
((sinh . y) * (cosh z)) + ((cosh y) * (sinh z))
by SIN_COS2:def 2
.=
((sinh . y) * (cosh z)) + ((cosh y) * (sinh . z))
by SIN_COS2:def 2
.=
((sinh . y) * (cosh . z)) + ((cosh y) * (sinh . z))
by SIN_COS2:def 4
.=
((sinh . y) * (cosh . z)) + ((cosh . y) * (sinh . z))
by SIN_COS2:def 4
.=
sinh . (y + z)
by SIN_COS2:21
.=
sinh (y + z)
by SIN_COS2:def 2
;
A3: tanh (y - z) =
tanh . (y - z)
by SIN_COS2:def 6
.=
((tanh . y) - (tanh . z)) / (1 - ((tanh . y) * (tanh . z)))
by SIN_COS2:22
.=
((tanh y) - (tanh . z)) / (1 - ((tanh . y) * (tanh . z)))
by SIN_COS2:def 6
.=
((tanh y) - (tanh z)) / (1 - ((tanh . y) * (tanh . z)))
by SIN_COS2:def 6
.=
((tanh y) - (tanh z)) / (1 - ((tanh y) * (tanh . z)))
by SIN_COS2:def 6
.=
((tanh y) - (tanh z)) / (1 - ((tanh y) * (tanh z)))
by SIN_COS2:def 6
;
A4: tanh (y + z) =
tanh . (y + z)
by SIN_COS2:def 6
.=
((tanh . y) + (tanh . z)) / (1 + ((tanh . y) * (tanh . z)))
by SIN_COS2:22
.=
((tanh y) + (tanh . z)) / (1 + ((tanh . y) * (tanh . z)))
by SIN_COS2:def 6
.=
((tanh y) + (tanh z)) / (1 + ((tanh . y) * (tanh . z)))
by SIN_COS2:def 6
.=
((tanh y) + (tanh z)) / (1 + ((tanh y) * (tanh . z)))
by SIN_COS2:def 6
.=
((tanh y) + (tanh z)) / (1 + ((tanh y) * (tanh z)))
by SIN_COS2:def 6
;
A5: ((sinh y) * (cosh z)) - ((cosh y) * (sinh z)) =
((sinh . y) * (cosh z)) - ((cosh y) * (sinh z))
by SIN_COS2:def 2
.=
((sinh . y) * (cosh z)) - ((cosh y) * (sinh . z))
by SIN_COS2:def 2
.=
((sinh . y) * (cosh . z)) - ((cosh y) * (sinh . z))
by SIN_COS2:def 4
.=
((sinh . y) * (cosh . z)) - ((cosh . y) * (sinh . z))
by SIN_COS2:def 4
.=
sinh . (y - z)
by SIN_COS2:21
.=
sinh (y - z)
by SIN_COS2:def 2
;
((cosh y) * (cosh z)) + ((sinh y) * (sinh z)) =
((cosh . y) * (cosh z)) + ((sinh y) * (sinh z))
by SIN_COS2:def 4
.=
((cosh . y) * (cosh . z)) + ((sinh y) * (sinh z))
by SIN_COS2:def 4
.=
((cosh . y) * (cosh . z)) + ((sinh . y) * (sinh z))
by SIN_COS2:def 2
.=
((cosh . y) * (cosh . z)) + ((sinh . y) * (sinh . z))
by SIN_COS2:def 2
.=
cosh . (y + z)
by SIN_COS2:20
.=
cosh (y + z)
by SIN_COS2:def 4
;
hence
( cosh (y + z) = ((cosh y) * (cosh z)) + ((sinh y) * (sinh z)) & cosh (y - z) = ((cosh y) * (cosh z)) - ((sinh y) * (sinh z)) & sinh (y + z) = ((sinh y) * (cosh z)) + ((cosh y) * (sinh z)) & sinh (y - z) = ((sinh y) * (cosh z)) - ((cosh y) * (sinh z)) & tanh (y + z) = ((tanh y) + (tanh z)) / (1 + ((tanh y) * (tanh z))) & tanh (y - z) = ((tanh y) - (tanh z)) / (1 - ((tanh y) * (tanh z))) )
by A1, A2, A5, A4, A3; verum