let x1, x2 be Real; :: thesis: ( sinh x1 <> 0 & sinh x2 <> 0 implies coth (x1 - x2) = (1 - ((coth x1) * (coth x2))) / ((coth x1) - (coth x2)) )
assume that
A1: sinh x1 <> 0 and
A2: sinh x2 <> 0 ; :: thesis: coth (x1 - x2) = (1 - ((coth x1) * (coth x2))) / ((coth x1) - (coth x2))
- (sinh . x2) <> 0 by A2, SIN_COS2:def 2;
then sinh . (- x2) <> 0 by SIN_COS2:19;
then A3: sinh (- x2) <> 0 by SIN_COS2:def 2;
coth (x1 - x2) = coth (x1 + (- x2))
.= (1 + ((coth x1) * (coth (- x2)))) / ((coth x1) + (coth (- x2))) by A1, A3, Th40
.= (1 + ((coth x1) * (- (coth x2)))) / ((coth x1) + (coth (- x2))) by Lm1
.= (1 - ((coth x1) * (coth x2))) / ((coth x1) + (- (coth x2))) by Lm1
.= (1 - ((coth x1) * (coth x2))) / ((coth x1) - (coth x2)) ;
hence coth (x1 - x2) = (1 - ((coth x1) * (coth x2))) / ((coth x1) - (coth x2)) ; :: thesis: verum