ABCD外切于⊙I，AIC∈⊙E，⊙E与BA,AD,BC,CD交于X,Y,Z,U，证 AD+DT+TX+XA=CD+DY+YZ+ZC

天山草

四边形 ABCD 有内切圆 I，圆AIC = 圆E，X = BA∩圆E，Y = AD∩圆E，Z = BC∩圆E，T = CD∩圆E。
证明 AD + DT + TX + XA = CD + DY + YZ + ZC。(2021 - IMO - 4)

天山草

添加辅助线以后的图：

程序图片：

天山草

程序代码：

1. Clear["Global`*"]; (*设B在坐标原点，C在1点， kAB=u^2，kA1C=1/v^2，kCA=w^2 *)
   
2. \!\(\*OverscriptBox[\(b\), \(_\)]\) = b = 0; \!\(\*OverscriptBox[\(c\), \(_\)]\) = c = 1; a1 = (u^2 (v^2 - 1))/( u^2 v^2 - 1);
   
3. \!\(\*OverscriptBox[\(a1\), \(_\)]\) = (v^2 - 1)/( u^2 v^2 - 1); Print["A1 = ", a1];
   
4. kAB = u^2; kA1C = 1/v^2; kCA = w^2;i = (u (v - 1))/(u v - 1); \!\(\*OverscriptBox[\(i\), \(_\)]\) = (v - 1)/(u v - 1); Print["I = ", i];
   
5. p = ((u + 1) (v - 1))/(2 u v - 2);  \!\(\*OverscriptBox[\(p\), \(_\)]\) = p; f = (u (u + 1) (v - 1))/( 2 u v - 2);  
   
6. \!\(\*OverscriptBox[\(f\), \(_\)]\) = ((u + 1) (v - 1))/(2 u (u v - 1));
   
7. Print["P = ", p]; Print["F = ", f];
   
8. k[a_, b_] := (a - b)/(\!\(\*OverscriptBox[\(a\), \(_\)]\) - \!\(\*OverscriptBox[\(b\), \(_\)]\)); (*复斜率定义*)
   
9. (*过A1点、复斜率等于k1的直线，与过A2点、复斜率等于k2的直线的交点：*)
   
10. Jd[k1_, a1_, k2_, a2_] := -((k2 (a1 - k1 \!\(\*OverscriptBox[\(a1\), \(_\)]\)) - k1 (a2 - k2 \!\(\*OverscriptBox[\(a2\), \(_\)]\)))/(k1 - k2));
    
11. \!\(\*OverscriptBox[\(Jd\), \(_\)]\)[k1_, a1_, k2_, a2_] := -((a1 - k1 \!\(\*OverscriptBox[\(a1\), \(_\)]\) - (a2 - k2 \!\(\*OverscriptBox[\(a2\), \(_\)]\)))/(k1 - k2));
    
12. Jx1[p_, a_, k_] := -k \!\(\*OverscriptBox[\(a\), \(_\)]\) + k \!\(\*OverscriptBox[\(p\), \(_\)]\) + a;  (*P点的镜线P1，镜线过点A且复斜率为k*)
    
13. \!\(\*OverscriptBox[\(Jx1\), \(_\)]\)[p_, a_, k_] := (k \!\(\*OverscriptBox[\(a\), \(_\)]\) - a + p)/k;
    
14. a = Simplify@Jd[kCA, c, kAB, b]; \!\(\*OverscriptBox[\(a\), \(_\)]\) = Simplify@\!\(\*OverscriptBox[\(Jd\), \(_\)]\)[kCA, c, kAB, b]; Print["A = ", a];
    
15. p1 = Simplify@Jx1[p, i, k[c, i]]; \!\(\*OverscriptBox[\(p1\), \(_\)]\) = Simplify@\!\(\*OverscriptBox[\(Jx1\), \(_\)]\)[p, i, k[c, i]]; Print["P1 = ", p1];
    
16. f1 = Simplify@Jx1[f, i, k[a, i]]; \!\(\*OverscriptBox[\(f1\), \(_\)]\) = Simplify@\!\(\*OverscriptBox[\(Jx1\), \(_\)]\)[f, i, k[a, i]]; Print["F1 = ", f1];
    
17. d = Simplify@Jd[k[a, f1], f1, k[c, p1], p1]; \!\(\*OverscriptBox[\(d\), \(_\)]\) = Simplify@\!\(\*OverscriptBox[\(Jd\), \(_\)]\)[k[a, f1], f1, k[c, p1], p1]; Print["D = ", d];
    
18. WX[a_, b_, c_] := (a \!\(\*OverscriptBox[\(a\), \(_\)]\) (c - b) + b \!\(\*OverscriptBox[\(b\), \(_\)]\) (a - c) + c \!\(\*OverscriptBox[\(c\), \(_\)]\) (b - a) )/(\!\(\*OverscriptBox[\(a\), \(_\)]\) (c - b) + \!\(\*OverscriptBox[\(b\), \(_\)]\) (a - c) + \!\(\*OverscriptBox[\(c\), \(_\)]\) (b - a));(*三角形 ABC 的外心坐标：*)   
    
19. \!\(\*OverscriptBox[\(WX\), \(_\)]\)[a_, b_, c_] := (\!\(\*OverscriptBox[\(a\), \(_\)]\) \!\(\*OverscriptBox[\(b\), \(_\)]\) (a - b) + \!\(\*OverscriptBox[\(b\), \(_\)]\) \!\(\*OverscriptBox[\(c\), \(_\)]\) (b - c) + \!\(\*OverscriptBox[\(c\), \(_\)]\) \!\(\*OverscriptBox[\(a\), \(_\)]\) (c - a))/(\!\(\*OverscriptBox[\(a\), \(_\)]\) (c - b) + \!\(\*OverscriptBox[\(b\), \(_\)]\) (a - c) + \!\(\*OverscriptBox[\(c\), \(_\)]\) (b - a));
    
20. e = Simplify@WX[a, i, c]; \!\(\*OverscriptBox[\(e\), \(_\)]\) = Simplify@\!\(\*OverscriptBox[\(WX\), \(_\)]\)[a, i, c];
    
21. Print["E = ", e];
    
22. x = Simplify@Jx1[a, e, -k[a, b]]; \!\(\*OverscriptBox[\(x\), \(_\)]\) = Simplify@\!\(\*OverscriptBox[\(Jx1\), \(_\)]\)[a, e, -k[a, b]]; Print["X = ", x];
    
23. y = Simplify@Jx1[a, e, -k[a, d]]; \!\(\*OverscriptBox[\(y\), \(_\)]\) = Simplify@\!\(\*OverscriptBox[\(Jx1\), \(_\)]\)[a, e, -k[a, d]]; Print["Y = ", y];
    
24. z = Simplify@Jx1[c, e, -1]; \!\(\*OverscriptBox[\(z\), \(_\)]\) = Simplify@\!\(\*OverscriptBox[\(Jx1\), \(_\)]\)[c, e, -1]; Print["Z = ", z];
    
25. t = Simplify@Jx1[c, e, -k[c, d]]; \!\(\*OverscriptBox[\(t\), \(_\)]\) = Simplify@\!\(\*OverscriptBox[\(Jx1\), \(_\)]\)[c, e, -k[c, d]]; Print["T = ", t];
    
26. AD = Simplify[Sqrt[(a - d) (\!\(\*OverscriptBox[\(a\), \(_\)]\) - \!\(\*OverscriptBox[\(d\), \(_\)]\))]]; AD = ((1 - u) (v w^2 + u (v - 1) - 1) ((v - 1) w^2 + u (v w^2 - 1)))/((u^2 - w^2) (u v^2 w^2 + v^2 w^2 - 2 v w^2 + u - 2 u v + 1)); Print["AD = ", AD];
    
27. TD = Simplify[Sqrt[(t - d) (\!\(\*OverscriptBox[\(t\), \(_\)]\) - \!\(\*OverscriptBox[\(d\), \(_\)]\))]]; TD = ((u - 1) (v - 1) (v (-v^2 w^2 + v w^2 + v - 1) w^4 - u ((w^4 + w^2) v^3 - 5 w^2 v^2 + 2 (w^2 + 1) v - 1) w^2 + u^2 (-(v - 2) v^2 w^4 + (2 v^2 - 5 v + 1) w^2 + 1) + u^3 (v^2 w^2 - v (w^2 + 1) + 1)))/((u v - 1) (u^2 - w^2) (v w^2 - 1) (u v^2 w^2 + v^2 w^2 - 2 v w^2 + u - 2 u v + 1)); Print["TD = ", TD];
    
28. XT = Simplify[Sqrt[(x - t) (\!\(\*OverscriptBox[\(x\), \(_\)]\) - \!\(\*OverscriptBox[\(t\), \(_\)]\))]]; XT = ((1 - u) (v - 1) w (w^2 +     u))/((u^2 - w^2) (v w^2 - 1)); Print["XT = ", XT];
    
29. XA = Simplify[Sqrt[(x - a) (\!\(\*OverscriptBox[\(x\), \(_\)]\) - \!\(\*OverscriptBox[\(a\), \(_\)]\))]]; XA = ((u - 1) ((v - 1) v w^4 +
    
30.      u (v w^2 - 1)^2 - u^2 (v - 1)))/((u v - 1) (u^2 - w^2) (v w^2 - 1)); Print["XA = ", XA];
    
31. ZC = Simplify[Sqrt[(z - c) (\!\(\*OverscriptBox[\(z\), \(_\)]\) - \!\(\*OverscriptBox[\(c\), \(_\)]\))]]; ZC = (u (v - 1) (w^2 - 1) (u - v w^2))/((u v - 1) (u^2 - w^2) (v w^2 - 1)) - 1; Print["ZC = ", ZC];
    
32. YZ = Simplify[Sqrt[(y - z) (\!\(\*OverscriptBox[\(y\), \(_\)]\) - \!\(\*OverscriptBox[\(z\), \(_\)]\))]]; YZ = ((1 - u) (v - 1) w (w^2 +
    
33.      u))/((u^2 - w^2) (v w^2 - 1)); Print["YZ = ", YZ];
    
34. DY = Simplify[Sqrt[(d - y) (\!\(\*OverscriptBox[\(d\), \(_\)]\) - \!\(\*OverscriptBox[\(y\), \(_\)]\))]]; DY = ((1 - u) (v - 1) v (w^2 - 1) (u - v w^2))/((u v - 1) (v w^2 - 1) (u v^2 w^2 + v^2 w^2 - 2 v w^2 + u - 2 u v + 1)); Print["DY = ", DY];
    
35. CD = Simplify[Sqrt[(c - d) (\!\(\*OverscriptBox[\(c\), \(_\)]\) - \!\(\*OverscriptBox[\(d\), \(_\)]\))]]; CD = ((u - 1) v (w^2 - 1))/(
    
36. u v^2 w^2 + v^2 w^2 - 2 v w^2 + u - 2 u v + 1); Print["CD = ", CD];
    
37. L1 = Simplify[AD + TD + XT + XA]; Print["AD+TD+XT+XA = ", L1];
    
38. L2 = Simplify[CD + DY + YZ + ZC]; Print["CD+DY+YZ+ZC = ", L2];
    
39. Print["因此 AD+TD+XT+XA = CD+DY+YZ+ZC"];

复制代码

天山草

此题很有趣，那么多的点和线段长度，点的坐标表达式和长度表达式，竟然都是有理式表达！