let x be Real; :: thesis: ( x < 0 implies sinh (x / 2) = - (sqrt (((cosh x) - 1) / 2)) )
assume x < 0 ; :: thesis: sinh (x / 2) = - (sqrt (((cosh x) - 1) / 2))
then A1: x / 2 < 0 by XREAL_1:141;
sinh (x / 2) = - (- (sinh (x / 2)))
.= - (sqrt ((sinh (x / 2)) ^2)) by A1, SIN_COS5:47, SQUARE_1:23
.= - (sqrt ((sinh . (x / 2)) ^2)) by SIN_COS2:def 2
.= - (sqrt ((1 / 2) * ((cosh . (2 * (x / 2))) - 1))) by SIN_COS2:18
.= - (sqrt (((cosh . x) - 1) / 2))
.= - (sqrt (((cosh x) - 1) / 2)) by SIN_COS2:def 4 ;
hence sinh (x / 2) = - (sqrt (((cosh x) - 1) / 2)) ; :: thesis: verum