let x be Real; :: thesis: cosh (3 * x) = (4 * ((cosh x) |^ 3)) - (3 * (cosh x))
cosh (3 * x) = cosh . ((x + x) + x) by SIN_COS2:def 4
.= ((cosh . (2 * x)) * (cosh . x)) + ((sinh . (2 * x)) * (sinh . x)) by SIN_COS2:20
.= (((2 * ((cosh . x) ^2)) - 1) * (cosh . x)) + ((sinh . (2 * x)) * (sinh . x)) by SIN_COS2:23
.= (((2 * ((cosh . x) ^2)) - 1) * (cosh . x)) + (((2 * (sinh . x)) * (cosh . x)) * (sinh . x)) by SIN_COS2:23
.= (((2 * ((cosh . x) ^2)) - 1) * (cosh . x)) + ((2 * ((sinh . x) ^2)) * (cosh . x))
.= (((2 * ((cosh . x) ^2)) - 1) * (cosh . x)) + ((2 * (((cosh . x) ^2) - 1)) * (cosh . x)) by Lm3
.= (4 * (((cosh . x) * (cosh . x)) * (cosh . x))) - (3 * (cosh . x))
.= (4 * ((((cosh . x) |^ 1) * (cosh . x)) * (cosh . x))) - (3 * (cosh . x))
.= (4 * (((cosh . x) |^ (1 + 1)) * (cosh . x))) - (3 * (cosh . x)) by NEWTON:6
.= (4 * ((cosh . x) |^ (2 + 1))) - (3 * (cosh . x)) by NEWTON:6
.= (4 * ((cosh . x) |^ 3)) - (3 * (cosh x)) by SIN_COS2:def 4 ;
hence cosh (3 * x) = (4 * ((cosh x) |^ 3)) - (3 * (cosh x)) by SIN_COS2:def 4; :: thesis: verum