Different ways to prove $\cos A+\cos B + \cos C=1+4\sin \frac A2 \sin \frac B2\sin \frac C2$ I would like to find other ways to prove this identity
$$\cos A+\cos B + \cos C=1+4\sin \frac A2 \sin \frac B2\sin \frac C2$$
Where $A,B,C$ are angles of a triangle.
My way to prove it is by $A+B+C=\pi$. By using product to sum formula, $$2\cos \frac{A+B}{2}\cos\frac{A-B}{2}+\cos C=2\sin\frac C2\cos\frac{A-B}{2}+1-2\sin^2\frac C2$$
This can be trivially proved by factoring $2\sin\frac C2$ and a sum to product formula.
I would like to see if there's another approach such as


*

*Assuming $B=?, C=?$

*By cyclic polynomial? Since this is a cyclic identity

*Or even Vieta's formula?

 A: One method with Computer Algebra Systems is to use a
substitution and factorization. In our case, we want to prove

$$\cos A+\cos B + \cos C=1+4\sin \frac A2 \sin \frac B2\sin \frac C2$$
Where $\,A,B,C\,$ are angles of a triangle.

The first step is to define substitutions
$$ A = \frac{2\log(X)}i, \quad B = \frac{2\log(Y)}i,
\quad C = \frac{2\log(Z)}i. $$ Rewrite the original equation as
$$ \cos A+\cos B + \cos C-
\Big(1+4\sin \frac A2 \sin \frac B2\sin \frac C2\Big)=0,$$
use the substitutions, and factor the expression to get
$$ \frac{(Z - i\,X Y) (Y - i\,X Z) (X - i\,Y Z) (i - X Y Z)}{2X^2Y^2Z^2}.$$
This expression is zero iff $\, C=(-1)^{n+m}\pi+(-1)^n A+ (-1)^m B.\,$
A Wolfram Mathematica program to verify this is
Unprotect[C]; ClearAll[fX, fA, A, B, C, X, Y, Z];
A = 2*Log[X]/I; B = 2*Log[Y]/I; C = 2*Log[Z]/I;
fA[A_,B_,C_] := (Cos[A]+Cos[B]+Cos[C])-(1+4*Sin[A/2]*Sin[B/2]*Sin[C/2]);
fX[X_,Y_,Z_] := (Z-I*X*Y)*(Y-I*X*Z)*(X-I*Y*Z)*(I-X*Y*Z)/(2*X^2*Y^2*Z^2);
fA[A,B,C] == fX[X,Y,Z] // TrigToExp // Simplify
fA[A,B,#]& /@ {A+B+Pi, A-B-Pi, -A+B-Pi,-A-B+Pi} == {0,0,0,0} // Simplify

