let x be Real; :: thesis: ( sinh (2 * x) = (2 * (sinh x)) * (cosh x) & cosh (2 * x) = (2 * ((cosh x) ^2)) - 1 & tanh (2 * x) = (2 * (tanh x)) / (1 + ((tanh x) ^2)) )
A1: cosh (2 * x) = cosh . (2 * x) by SIN_COS2:def 4
.= (2 * ((cosh . x) ^2)) - 1 by SIN_COS2:23
.= (2 * ((cosh x) ^2)) - 1 by SIN_COS2:def 4 ;
A2: tanh (2 * x) = tanh . (2 * x) by SIN_COS2:def 6
.= (2 * (tanh . x)) / (1 + ((tanh . x) ^2)) by SIN_COS2:23
.= (2 * (tanh x)) / (1 + ((tanh . x) ^2)) by SIN_COS2:def 6
.= (2 * (tanh x)) / (1 + ((tanh x) ^2)) by SIN_COS2:def 6 ;
sinh (2 * x) = sinh . (2 * x) by SIN_COS2:def 2
.= (2 * (sinh . x)) * (cosh . x) by SIN_COS2:23
.= (2 * (sinh x)) * (cosh . x) by SIN_COS2:def 2
.= (2 * (sinh x)) * (cosh x) by SIN_COS2:def 4 ;
hence ( sinh (2 * x) = (2 * (sinh x)) * (cosh x) & cosh (2 * x) = (2 * ((cosh x) ^2)) - 1 & tanh (2 * x) = (2 * (tanh x)) / (1 + ((tanh x) ^2)) ) by A1, A2; :: thesis: verum