Proof of Theorem 5

(* ================== I N C E N T E R =============== *)

(* Given a, b, d, e, this returns t *)
Stewart[a_,b_,d_,e_]:=Sqrt[(a^2e+b^2d-(d+e) d e)/(d+e)];

(* Given a, b, c, this returns cos C *)
LawOfCosines[a_,b_,c_]=(a^2+b^2-c^2)/(2 a b);

(* Given AB, AC, BC with angle bisecto AD, returns BD, DC *)
FindAngleBisectorDivision[AB_,AC_,BC_]:=Module[{BD,DC},
BD=(AB/(AB+AC))BC;
DC=BC-BD;
Return[{BD,DC}];
];

Clear[K1,K2,K3,K4,K5,K6];
Clear[s1,s2,s3,s4,s5,s6];
Clear[a,b,c];
{a1,a2}=FindAngleBisectorDivision[c,b,a];
{b1,b2}=FindAngleBisectorDivision[a,c,b];
{c1,c2}=FindAngleBisectorDivision[b,a,c];
eq2=K2/K1==a2/a1;
eq3=(K1+K2)/K3==e/f;
eq4=K4/K3==b2/b1;
eq5=(K3+K4)/K5==g/h;
eq6=K6/K5==c2/c1;
AD=Map[Together,Simplify[Stewart[c,b,a1,a2]]]//PowerExpand;
BE=Map[Together,Simplify[Stewart[a,c,b1,b2]]]//PowerExpand;
CF=Map[Together,Simplify[Stewart[b,a,c1,c2]]]//PowerExpand;
{e,f}=FindAngleBisectorDivision[a,b1,BE]//Simplify;{g,h}=FindAngleBisectorDivision[a,c2,CF]//Simplify;
{j,k}=FindAngleBisectorDivision[a2,b,AD]//Simplify;
fixK=Solve[{eq2,eq3,eq4,eq5,eq6},{K2,K3,K4,K5,K6}][[1]];
cosalpha=LawOfCosines[c1,k,h];
cosbeta=LawOfCosines[a1,e,j];
cosgamma=LawOfCosines[b1,g,f];
fixs=
{s1->(1/2)(e+a1+j),
s2->(1/2)(g+a2+j),
s3->(1/2)(g+b1+f),
s4->(1/2)(k+b2+f),
s5->(1/2)(c1+h+k),
s6->(1/2)(c2+h+e)};
r1=K1/s1;
r2=K2/s2;
r3=K3/s3;
r4=K4/s4;
r5=K5/s5;
r6=K6/s6;
S=cosgamma(1/r1-1/r4)+cosalpha(1/r3-1/r6)+cosbeta(1/r5-1/r2);

S//Simplify

fixK

S2=Simplify[S/.fixK]

num=Numerator[S2]

num/.fixs//Simplify