let x1, x2, x3 be Real; :: thesis: ( sin x1 <> 0 & sin x2 <> 0 & sin x3 <> 0 implies cos ((x1 + x2) + x3) = - ((((sin x1) * (sin x2)) * (sin x3)) * ((((cot x1) + (cot x2)) + (cot x3)) - (((cot x1) * (cot x2)) * (cot x3)))) )
assume that
A1: sin x1 <> 0 and
A2: sin x2 <> 0 and
A3: sin x3 <> 0 ; :: thesis: cos ((x1 + x2) + x3) = - ((((sin x1) * (sin x2)) * (sin x3)) * ((((cot x1) + (cot x2)) + (cot x3)) - (((cot x1) * (cot x2)) * (cot x3))))
cos ((x1 + x2) + x3) = cos (x1 + (x2 + x3))
.= ((cos x1) * (cos (x2 + x3))) - ((sin x1) * (sin (x2 + x3))) by SIN_COS:75
.= ((cos x1) * (((cos x2) * (cos x3)) - ((sin x2) * (sin x3)))) - ((sin x1) * (sin (x2 + x3))) by SIN_COS:75
.= (((cos x1) * ((cos x2) * (cos x3))) - ((cos x1) * ((sin x2) * (sin x3)))) - ((sin x1) * (((sin x2) * (cos x3)) + ((cos x2) * (sin x3)))) by SIN_COS:75
.= ((((cos x1) * (cos x2)) * (cos x3)) - (((cos x1) * (sin x2)) * (sin x3))) - ((((sin x1) * (sin x2)) * (cos x3)) + (((sin x1) * (sin x3)) * (cos x2)))
.= ((((cos x1) * (cos x2)) * (cos x3)) - (((cos x1) * (sin x2)) * (sin x3))) - ((((sin x1) * (sin x2)) * ((sin x3) * (cot x3))) + (((sin x1) * (sin x3)) * (cos x2))) by A3, Th2
.= ((((cos x1) * (cos x2)) * (cos x3)) - (((cos x1) * (sin x2)) * (sin x3))) - ((((sin x1) * (sin x2)) * ((sin x3) * (cot x3))) + (((sin x1) * (sin x3)) * ((sin x2) * (cot x2)))) by A2, Th2
.= (((((sin x1) * (cot x1)) * (cos x2)) * (cos x3)) - (((cos x1) * (sin x2)) * (sin x3))) - ((((sin x1) * (sin x2)) * (sin x3)) * ((cot x3) + (cot x2))) by A1, Th2
.= (((((sin x1) * (cot x1)) * ((sin x2) * (cot x2))) * (cos x3)) - (((cos x1) * (sin x2)) * (sin x3))) - ((((sin x1) * (sin x2)) * (sin x3)) * ((cot x3) + (cot x2))) by A2, Th2
.= (((((sin x1) * (cot x1)) * ((sin x2) * (cot x2))) * ((sin x3) * (cot x3))) - (((cos x1) * (sin x2)) * (sin x3))) - ((((sin x1) * (sin x2)) * (sin x3)) * ((cot x3) + (cot x2))) by A3, Th2
.= (((((sin x1) * (sin x2)) * (sin x3)) * (((cot x1) * (cot x2)) * (cot x3))) - ((((sin x1) * (cot x1)) * (sin x2)) * (sin x3))) - ((((sin x1) * (sin x2)) * (sin x3)) * ((cot x3) + (cot x2))) by A1, Th2
.= - ((((sin x1) * (sin x2)) * (sin x3)) * ((((cot x1) + (cot x2)) + (cot x3)) - (((cot x1) * (cot x2)) * (cot x3)))) ;
hence cos ((x1 + x2) + x3) = - ((((sin x1) * (sin x2)) * (sin x3)) * ((((cot x1) + (cot x2)) + (cot x3)) - (((cot x1) * (cot x2)) * (cot x3)))) ; :: thesis: verum