let x be Real; :: thesis: ( sin x <> 0 implies cot (3 * x) = (((cot x) |^ 3) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1) )
assume A1: sin x <> 0 ; :: thesis: cot (3 * x) = (((cot x) |^ 3) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1)
cot (3 * x) = cot ((x + x) + x)
.= ((((((cot x) * (cot x)) * (cot x)) - (cot x)) - (cot x)) - (cot x)) / (((((cot x) * (cot x)) + ((cot x) * (cot x))) + ((cot x) * (cot x))) - 1) by A1, SIN_COS4:14
.= ((((cot x) * (cot x)) * (cot x)) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1)
.= (((((cot x) |^ 1) * (cot x)) * (cot x)) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1)
.= ((((cot x) |^ (1 + 1)) * (cot x)) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1) by NEWTON:6
.= (((cot x) |^ (2 + 1)) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1) by NEWTON:6 ;
hence cot (3 * x) = (((cot x) |^ 3) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1) ; :: thesis: verum