ABCD是具有内切圆和外接圆的四边形。圆E和圆F是△ABD和△CBD的内心。证明AEFC共圆。

天山草

ABCD 是同时具有内切圆和外接圆的四边形。圆E和圆F是△ABD和△CBD的内心。
证明AEFC共圆。

天山草

四边形有外接圆的充要条件是其对角互补。
四边形有内切圆的充要条件是其对边长度之和相等。证明中必须用到这个条件才行。

天山草

说明：初始程序中采用了三个变量：\(u、v、w\)，考虑到四边形具有内切圆这个条件，知两组对边

长度之和应该相等，按此约束，可找出 \(w\) 与\(u、v\) 的关系。因此最终变量只有\(u、v\) 这两个。

最后，判断四点共圆的依据是如果对应的两个圆周角相等则四点共圆。

1. Clear["Global`*"];(*令△ABC的外接圆为单位圆O，BC边平行于实轴。AB、AC、BD的复斜率为u^2,v^2,w^2*)
   
2. \!\(\*OverscriptBox[\(o\), \(_\)]\) = o = 0; a = I u v;   \!\(\*OverscriptBox[\(a\), \(_\)]\) = 1/(I u v); b = (I u)/v;  
   
3. \!\(\*OverscriptBox[\(b\), \(_\)]\) = v/(I u);  c = (I v)/u;  \!\(\*OverscriptBox[\(c\), \(_\)]\) = u/(I v);
   
4. Simplify@Solve[{(o - b) (\!\(\*OverscriptBox[\(o\), \(_\)]\) - \!\(\*OverscriptBox[\(b\), \(_\)]\)) == (o - d) (\!\(\*OverscriptBox[\(o\), \(_\)]\) - 1/d), (b - d)/(\!\(\*OverscriptBox[\(b\), \(_\)]\) - 1/d) == w^2}, {d}] // Flatten;
   
5. d = (I v w^2)/u; \!\(\*OverscriptBox[\(d\), \(_\)]\) = 1/d;
   
6. (*以下五条线段的最终长度公式中前面取正号还是取负号，需要代入具体数字进行判断。对于此图，u=0.5326+0.8463 I;
   
7. v=0.5534-0.8328 I; w=0.8526+0.5225 I;*)
   
8. AB = Factor@Simplify[Sqrt[(a - b) (\!\(\*OverscriptBox[\(a\), \(_\)]\) - \!\(\*OverscriptBox[\(b\), \(_\)]\))]]; AB = Sqrt[-((v^2 - 1)^2/  v^2)]; AB = (v^2 - 1)/v I;
   
9. BC = Factor@Simplify[ Sqrt[(b - c) (\!\(\*OverscriptBox[\(b\), \(_\)]\) - \!\(\*OverscriptBox[\(c\), \(_\)]\))]]; BC = Sqrt[-((u^2 - v^2)^2/(  u^2 v^2))]; BC = -((u^2 - v^2)/(u v)) I;
   
10. DC = Factor@Simplify[ Sqrt[(d - c) (\!\(\*OverscriptBox[\(d\), \(_\)]\) - \!\(\*OverscriptBox[\(c\), \(_\)]\))]]; DC = Sqrt[-((w^2 - 1)^2/  w^2)]; DC = -((w^2 - 1)/w) I;
    
11. AD = Factor@Simplify[Sqrt[(a - d) (\!\(\*OverscriptBox[\(a\), \(_\)]\) - \!\(\*OverscriptBox[\(d\), \(_\)]\))]]; AD = Sqrt[-((u^2 - w^2)^2/( u^2 w^2))]; AD = -((u^2 - w^2)/(u w)) I;
    
12. BD = Factor@Simplify[Sqrt[(b - d) (\!\(\*OverscriptBox[\(b\), \(_\)]\) - \!\(\*OverscriptBox[\(d\), \(_\)]\))]]; BD = Sqrt[-((u^2 -
    
13.     v^2 w^2)^2/(u^2 v^2 w^2))]; BD = -((u^2 - v^2 w^2)/(u v w)) I;
    
14. e = Simplify[(a BD + b AD + d AB)/(AB + BD + AD)]; \!\(\*OverscriptBox[\(e\), \(_\)]\) = Simplify[(\!\(\*OverscriptBox[\(a\), \(_\)]\) BD + \!\(\*OverscriptBox[\(b\), \(_\)]\) AD + \!\(\*OverscriptBox[\(d\), \(_\)]\) AB)/(AB + BD + AD)];
    
15. e =  I (u + (v - 1) w); \!\(\*OverscriptBox[\(e\), \(_\)]\) = (I (u (v - 1) - v w))/(u v w);
    
16. f = Simplify[(b DC + c BD + d BC)/(BC + DC + BD)]; \!\(\*OverscriptBox[\(f\), \(_\)]\) = Simplify[(\!\(\*OverscriptBox[\(b\), \(_\)]\) DC + \!\(\*OverscriptBox[\(c\), \(_\)]\) BD + \!\(\*OverscriptBox[\(d\), \(_\)]\) BC)/(BC + DC + BD)];
    
17. f = ( I (u (w - 1) + v w))/u; \!\(\*OverscriptBox[\(f\), \(_\)]\) = -((I (u - v w + v))/(v w));
    
18. k[a_, b_] := (a - b)/(\!\(\*OverscriptBox[\(a\), \(_\)]\) - \!\(\*OverscriptBox[\(b\), \(_\)]\));(*定义复斜率*)
    
19. Simplify@Solve[{AD + BC == AB + DC }, {w}] // Flatten;
    
20. w = (u^2 + Sqrt[u^4 + u^3 (6 v^2 - 2) + u^2 (v^4 + 4 v^2 + 1) - 2 u v^2 (v^2 - 3) + v^4] + u (v^2 - 1) - v^2)/(2 (u + 1) v);
    
21. d = Factor@Simplify[(I v w^2)/u]; \!\(\*OverscriptBox[\(d\), \(_\)]\) = 1/d;
    
22. e = Factor@Simplify[I (u + (v - 1) w)]; \!\(\*OverscriptBox[\(e\), \(_\)]\) = Factor@Simplify[(I (u (v - 1) - v w))/(u v w)];
    
23. f = Factor@Simplify[(I (u (w - 1) + v w))/u]; \!\(\*OverscriptBox[\(f\), \(_\)]\) = Factor@Simplify[-((I (u - v w + v))/(v w))];
    
24. Print["a = ", a, "， b = ", b, "， c = ", c, "， d = ", d]; Print["e = ", e]; Print["f = ", f];
    
25. f\[Angle][a_, b_, c_] := k[b, c]/k[a, b];  (*左边表示∠ABC的指数函数\[ExponentialE]^\[ImaginaryI]2\[Angle]ABC*)
    
26. f\[Angle]AEC = Factor@FullSimplify[ f\[Angle][a, e, c]];
    
27. f\[Angle]AFC = Factor@FullSimplify[ f\[Angle][a, f, c] ];
    
28. Print["f\[Angle]AEC = ", f\[Angle]AEC];
    
29. Print["f\[Angle]AFC = ", f\[Angle]AFC];
    
30. Print["由于 f\[Angle]AEC = f\[Angle]AFC，所以 AEFC 四点共圆。"]

复制代码