ABCD是圆 I 的外切四边形，AB交CD于E，圆EBC与圆AED交于F。求证 IF 是∠BFD的平分线

天山草

构图和设点： 将E点置于坐标系原点，ED  与实轴重合，D点坐标为 1。

用 mathematica 写的证明程序：



程序运行结果：

天山草

程序代码：

1. Clear["Global`*"];  (*将E点置于坐标系原点，D点坐标为 1，AE的复斜率为kAE=u^4，AD的复斜率为kAD=1/v^4*)
   
2. \!\(\*OverscriptBox[\(e\), \(_\)]\) = e = 0; \!\(\*OverscriptBox[\(d\), \(_\)]\) = d = 1; a = (u^4 (v^4 - 1))/( u^4 v^4 - 1);
   
3. \!\(\*OverscriptBox[\(a\), \(_\)]\) = (v^4 - 1)/( u^4 v^4 - 1); (*\[EmptyUpTriangle]AED的顶点坐标*)
   
4. i = (u^2 (v^2 - 1))/(u^2 v^2 - 1); \!\(\*OverscriptBox[\(i\), \(_\)]\) = (v^2 - 1)/( u^2 v^2 - 1); (*\[EmptyUpTriangle]AED的内心坐标:*)
   
5. (*在此构图下，有上面的已知公式可引用*)
   
6. c = \[Lambda] d + (1 - \[Lambda]) e; \!\(\*OverscriptBox[\(c\), \(_\)]\) = \[Lambda] \!\(\*OverscriptBox[\(d\), \(_\)]\) + (1 - \[Lambda]) \!\(\*OverscriptBox[\(e\), \(_\)]\); (*设C点坐标，\[Lambda] 是 0 到 1 之间的实数*)
   
7. k[a_, b_] := (a - b)/(\!\(\*OverscriptBox[\(a\), \(_\)]\) - \!\(\*OverscriptBox[\(b\), \(_\)]\));(*复斜率定义*)  kIC =  k[i, c];(*IC线的复斜率*)kCD = 1;(*CD线的复斜率*)
   
8. kBC = kIC^2/ kCD; (*因为IC是\[Angle]BCD的平分线，所以kIC^2=kBC\[Times]kCD，故kBC=kIC^2/kCD *)
   
9. Jd[k1_, a1_, k2_, a2_] := -((k2 (a1 - k1 \!\(\*OverscriptBox[\(a1\), \(_\)]\)) - k1 (a2 - k2 \!\(\*OverscriptBox[\(a2\), \(_\)]\)))/(k1 - k2));
   
10. \!\(\*OverscriptBox[\(Jd\), \(_\)]\)[k1_, a1_, k2_, a2_] := -((a1 - k1 \!\(\*OverscriptBox[\(a1\), \(_\)]\) - (a2 - k2 \!\(\*OverscriptBox[\(a2\), \(_\)]\)))/(k1 - k2));
    
11. (*复斜率等于k1且经过A1点的直线，与复斜率等于k2且经过A2点的直线，两直线的交点*)
    
12. b = Simplify@Jd[kBC, c, k[a, e], a]; \!\(\*OverscriptBox[\(b\), \(_\)]\) = Simplify@\!\(\*OverscriptBox[\(Jd\), \(_\)]\)[kBC, c, k[a, e], a];
    
13. Yuan[a1_, b1_,    c1_] := (( (z - b1) (a1 - c1))/( (z - c1) (a1 - b1)) - ( (\!\(\*OverscriptBox[\(z\), \(_\)]\) - \!\(\*OverscriptBox[\(b1\), \(_\)]\)) (\!\(\*OverscriptBox[\(a1\), \(_\)]\) - \!\(\*OverscriptBox[\(c1\), \(_\)]\)))/( (\!\(\*OverscriptBox[\(z\), \(_\)]\) - \!\(\*OverscriptBox[\(c1\), \(_\)]\)) (\!\(\*OverscriptBox[\(a1\), \(_\)]\) - \!\(\*OverscriptBox[\(b1\), \(_\)]\)))); (* 此表达式等于零即是经过A1B1C1三点的圆方程 *)
    
14. W = {z, \!\(\*OverscriptBox[\(z\), \(_\)]\)} /.     Solve[{Yuan[e, b, c] == 0, Yuan[a, e, d] == 0, z != e}, {z, \!\(\*OverscriptBox[\(z\), \(_\)]\)}] // Flatten;
    
15. f = Part[W, 1]; \!\(\*OverscriptBox[\(f\), \(_\)]\) = Part[W, 2];  Print["F = ", f];
    
16. Print["IF 线复斜率的平方 = ", Simplify[k[i, f]^2]];
    
17. Print["BF 的复斜率与 DF 的复斜率之积 = ", Simplify[k[b, f] k[d, f]]];
    
18. Print["测试上面二式是否相等："];
    
19. Simplify[k[i, f]^2 == k[b, f] k[d, f]]
    
20. Print["由于 BF 的复斜率与 DF 的复斜率之积相等，所以 IF 是 \[Angle]BFD 的平分线。 "];

复制代码