数学研发论坛

 找回密码
 欢迎注册
查看: 280|回复: 6

[原创] 四条验证i机器证明的高难度定理

[复制链接]
发表于 2021-12-12 21:35:12 | 显示全部楼层 |阅读模式

马上注册,结交更多好友,享用更多功能,让你轻松玩转社区。

您需要 登录 才可以下载或查看,没有帐号?欢迎注册

x
1  五圆定理 2莫利定理3Lemoine 圆定理4,泰博定理
毋因群疑而阻独见  毋任己意而废人言
毋私小惠而伤大体  毋借公论以快私情
 楼主| 发表于 2021-12-14 20:15:15 | 显示全部楼层
本帖最后由 dlsh 于 2021-12-14 20:18 编辑

五圆定理证明

设G是△ABC的重心,K是陪位重心,过K作三边的平行线l1,l2,l3(图1),这种平行线称为勒穆瓦纳平行线。
Lemoine circle1.gif 三条勒穆瓦纳平行线与三角形周界的六个交点在同一个圆上,这个圆称为这个三角形的第一勒穆瓦纳圆,该圆在三角形三边上所截的弦与三边的立方成比例,故又称为三重比圆。

  1. Clear["Global`*"]

  2. \!\(\*OverscriptBox["a", "_"]\) = 1/a;
  3. \!\(\*OverscriptBox["b", "_"]\) = 1/b;
  4. \!\(\*OverscriptBox["c", "_"]\) = 1/c; g = (a + b + c)/3;
  5. \!\(\*OverscriptBox["g", "_"]\) = (
  6. \!\(\*OverscriptBox["a", "_"]\) +
  7. \!\(\*OverscriptBox["b", "_"]\) +
  8. \!\(\*OverscriptBox["c", "_"]\))/3;
  9. k[a_, b_] := (a - b)/(
  10. \!\(\*OverscriptBox["a", "_"]\) -
  11. \!\(\*OverscriptBox["b", "_"]\));
  12. \!\(\*OverscriptBox["k", "_"]\)[a_, b_] := 1/k[a, b];(*复斜率定义*)
  13. k1 = (a^2 b c)/k[g, a]; k2 = (b^2 a c)/k[g, b];

  14. \!\(\*OverscriptBox["Jd", "_"]\)[k1_, a1_, k2_, a2_] := -((a1 - k1
  15. \!\(\*OverscriptBox["a1", "_"]\) - (a2 - k2
  16. \!\(\*OverscriptBox["a2", "_"]\)))/(
  17.   k1 - k2));(*复斜率等于k1,过点A1与复斜率等于k2,过点A2的直线交点*)
  18. Jd[k1_, a1_, k2_, a2_] := -((k2 (a1 - k1
  19. \!\(\*OverscriptBox["a1", "_"]\)) - k1 (a2 - k2
  20. \!\(\*OverscriptBox["a2", "_"]\)))/(k1 - k2));
  21. Waixin[a_, b_, c_] := (a
  22. \!\(\*OverscriptBox["a", "_"]\) (b - c) + b
  23. \!\(\*OverscriptBox["b", "_"]\) (c - a) + c
  24. \!\(\*OverscriptBox["c", "_"]\) (a - b) )/(
  25. \!\(\*OverscriptBox["a", "_"]\) (b - c) +
  26. \!\(\*OverscriptBox["b", "_"]\) (c - a) +
  27. \!\(\*OverscriptBox["c", "_"]\) (a - b));
  28. \!\(\*OverscriptBox["Waixin", "_"]\)[a_, b_, c_] := -((a
  29. \!\(\*OverscriptBox["a", "_"]\) (
  30. \!\(\*OverscriptBox["b", "_"]\) -
  31. \!\(\*OverscriptBox["c", "_"]\)) + b
  32. \!\(\*OverscriptBox["b", "_"]\) (
  33. \!\(\*OverscriptBox["c", "_"]\) -
  34. \!\(\*OverscriptBox["a", "_"]\)) + c
  35. \!\(\*OverscriptBox["c", "_"]\) (
  36. \!\(\*OverscriptBox["a", "_"]\) -
  37. \!\(\*OverscriptBox["b", "_"]\)) )/(
  38. \!\(\*OverscriptBox["a", "_"]\) (b - c) +
  39. \!\(\*OverscriptBox["b", "_"]\) (c - a) +
  40. \!\(\*OverscriptBox["c", "_"]\) (a - b)));
  41. k = Jd[k1, a, k2, b];
  42. \!\(\*OverscriptBox["k", "_"]\) =
  43. \!\(\*OverscriptBox["Jd", "_"]\)[k1, a, k2, b];
  44. L = Jd[-a b, a, -b c, k];
  45. \!\(\*OverscriptBox["L", "_"]\) =
  46. \!\(\*OverscriptBox["Jd", "_"]\)[-a b, a, -b c, k]; t =
  47. Jd[-a b, a, -a c, k];
  48. \!\(\*OverscriptBox["t", "_"]\) =
  49. \!\(\*OverscriptBox["Jd", "_"]\)[-a b, a, -a c, k];
  50. p = Jd[-a b, k, -b c, b];
  51. \!\(\*OverscriptBox["p", "_"]\) =
  52. \!\(\*OverscriptBox["Jd", "_"]\)[-a b, k, -b c, b]; s =
  53. Jd[-c b, b, -a c, k];
  54. \!\(\*OverscriptBox["s", "_"]\) =
  55. \!\(\*OverscriptBox["Jd", "_"]\)[-c b, b, -a c, k];
  56. o1 = Waixin[t, L, p];
  57. \!\(\*OverscriptBox["o1", "_"]\) =
  58. \!\(\*OverscriptBox["Waixin", "_"]\)[t, L, p];
  59. Simplify[{k,
  60. \!\(\*OverscriptBox["k", "_"]\)}]
  61. Simplify[{1, t,
  62. \!\(\*OverscriptBox["t", "_"]\), , L,
  63. \!\(\*OverscriptBox[
  64. RowBox[{"L", "\[IndentingNewLine]"}], "_"]\), , p,
  65. \!\(\*OverscriptBox["p", "_"]\), , s,
  66. \!\(\*OverscriptBox["s", "_"]\)}]
  67. Simplify[{2, o1,
  68. \!\(\*OverscriptBox["o1", "_"]\), , (o1 - t) (
  69. \!\(\*OverscriptBox["o1", "_"]\) -
  70. \!\(\*OverscriptBox["t", "_"]\))}]
  71. Factor[{2, o1,
  72. \!\(\*OverscriptBox["o1", "_"]\), , (o1 - t) (
  73. \!\(\*OverscriptBox["o1", "_"]\) -
  74. \!\(\*OverscriptBox["t", "_"]\))}]
  75. Simplify[{3, t - L, s - p, , (t - L)/(s - p)}]


复制代码

Lemoine circle.gif
毋因群疑而阻独见  毋任己意而废人言
毋私小惠而伤大体  毋借公论以快私情
发表于 2021-12-17 15:10:55 | 显示全部楼层
本帖最后由 TSC999 于 2021-12-17 16:40 编辑

下面用楼主的基本方法证明泰博定理。

证明泰博定理构图.png

构图说明.png

  1. Clear["Global`*"];  (*三个自由变量 u,v,w,其中 w^2 是 CN 的复斜率 *)
  2. i0 = 0;
  3. \!\(\*OverscriptBox[\(i0\), \(_\)]\) = 0;(*三角形ABC的内切圆为单位圆,I0 为内心*)
  4. a = u - I; b = v - I;  
  5. \!\(\*OverscriptBox[\(a\), \(_\)]\) = u + I;
  6. \!\(\*OverscriptBox[\(b\), \(_\)]\) = v + I;
  7. c = ((u + v) + I (v u - 1))/(u v + 1);
  8. \!\(\*OverscriptBox[\(c\), \(_\)]\) = ((u + v) - I (v u - 1))/(
  9. u v + 1);(*采用已知公式:三角形ABC的C点复坐标*)  Print["c = ", c];
  10. o = ((u - I) (v - I) (I v u + u + v + 3 I))/(4 (u v + 1));  
  11. \!\(\*OverscriptBox[\(o\), \(_\)]\) = ((u + I) (v + I) (-I u v + u +
  12.     v - 3 I))/(
  13. 4 (u v + 1)); (* 采用已知公式:三角形ABC的外接圆圆心O点复坐标*) Print["o = ", o];
  14. R = -(((1 + u^2) (1 + v^2))/(
  15.   4 (1 + u v)));  (* 采用已知公式:三角形ABC外接圆的半径 R *)  Print["外接圆半径 R = ", R];
  16. kf[a_, b_] := (a - b)/(
  17. \!\(\*OverscriptBox[\(a\), \(_\)]\) -
  18. \!\(\*OverscriptBox[\(b\), \(_\)]\));
  19. \!\(\*OverscriptBox[\(kf\), \(_\)]\)[a_, b_] :=
  20. 1/kf[a, b]; (* AB 直线的复斜率 *)
  21. (* 以下求角ANC平分线 m 的复斜率, 由于AB的复斜率 kab=1,CN的复斜率 knc=w^2, 所以角平分线的复斜率 km=w  \
  22. *)
  23. (* 角ANB平分线 n 与 m 垂直,所以直线 n 的复斜率=-w。另外因直线 KI0//n,故 KI0的复斜率也等于 -w *)
  24. km = w; kn = -w; kcn = w^2;
  25. Jd[k1_, a1_, k2_, a2_] := -((k2 (a1 - k1
  26. \!\(\*OverscriptBox[\(a1\), \(_\)]\)) - k1 (a2 - k2
  27. \!\(\*OverscriptBox[\(a2\), \(_\)]\)))/(k1 - k2));

  28. \!\(\*OverscriptBox[\(Jd\), \(_\)]\)[k1_, a1_, k2_, a2_] := -((a1 - k1
  29. \!\(\*OverscriptBox[\(a1\), \(_\)]\) - (a2 - k2
  30. \!\(\*OverscriptBox[\(a2\), \(_\)]\)))/(  
  31.       k1 - k2)); (*复斜率等于k1,过点A1与复斜率等于k2,过点A2的直线交点*)
  32. n = Simplify@ Jd[kcn, c, 1, a];
  33. \!\(\*OverscriptBox[\(n\), \(_\)]\) = Simplify@
  34. \!\(\*OverscriptBox[\(Jd\), \(_\)]\)[kcn, c, 1, a]; Print["n = ", n];
  35. k = Simplify@ Jd[kn, i0, 1, a];
  36. \!\(\*OverscriptBox[\(k\), \(_\)]\) = Simplify@
  37. \!\(\*OverscriptBox[\(Jd\), \(_\)]\)[kn, i0, 1, a]; Print["k = ", k];
  38. p = Simplify@ Jd[km, i0, 1, a];
  39. \!\(\*OverscriptBox[\(p\), \(_\)]\) = Simplify@
  40. \!\(\*OverscriptBox[\(Jd\), \(_\)]\)[km, i0, 1, a]; Print["p = ", p];
  41. (* 以下求 I1 点的复坐标。它是两直线的交点,一条是复斜率为-1、经过K点的线,另一条是复斜率为 km、经过N点的线 *)
  42. i1 = Simplify@ Jd[-1, k, km, n];
  43. \!\(\*OverscriptBox[\(i1\), \(_\)]\) = Simplify@
  44. \!\(\*OverscriptBox[\(Jd\), \(_\)]\)[-1, k, km,
  45.    n]; Print["i1 = ", i1];
  46. (* 以下求 I2 点的复坐标。它是两直线的交点,一条是复斜率为-1、经过P点的线,另一条是复斜率为 kn、经过N点的线 *)
  47. i2 = Simplify@ Jd[-1, p, kn, n];
  48. \!\(\*OverscriptBox[\(i2\), \(_\)]\) = Simplify@
  49. \!\(\*OverscriptBox[\(Jd\), \(_\)]\)[-1, p, kn, n]; Print["i2 = ", i2];
  50. ki1i0 = Simplify[kf[i1, i0]];
  51. ki0i2 = Simplify[kf[i2, i0]]; (* 证明 I1、I0、I2 三点共线 *)
  52. Print["I1I0的复斜率 =", ki1i0]; Print["I0I2的复斜率 =", ki0i2];
  53. If[ki1i0 == ki0i2,
  54.   Print["由于 I1I0 的复斜率等于 I0I2 的复斜率,所以 I1、I0、I2 三点共线。"]];
  55. S[a_, b_] := Sqrt[(a - b) (
  56. \!\(\*OverscriptBox[\(a\), \(_\)]\) -
  57. \!\(\*OverscriptBox[\(b\), \(_\)]\))];  (* A、B 点间的距离 *)
  58. (* 以I1为圆心、I1K为半径作圆I1; 以I2为圆心、I2P为半径作圆I2,则两圆都与BC和CN相切 *)
  59. (* 以下证明I1圆和I2圆都与O圆相内切 *)
  60. S1 = Simplify@S[o, i1];   (* I1圆和O圆连心线长度,未简化 *)
  61. S2 = Simplify@S[o, i2] ; (* I2圆和O圆连心线长度,未简化 *)
  62. S1 = (-3 w^2 + 10 w + v^2 (w + 1)^2 + u^2 (v^2 + 1) (w + 1)^2 +
  63.    4 I v (w^2 - 1) + 4 u (w + 1) (I (w - 1) + v (w + 1)) -
  64.    3)/(-4 (u v + 1) (w + 1)^2); (* 人工协助简化结果 *)
  65. S2 = (v^2 (w - 1)^2 + u^2 (v^2 + 1) (w - 1)^2 +
  66.    4 u (v (w - 1) + I (w + 1)) (w - 1) - 3 w^2 - 10 w +
  67.    4 I v (w^2 - 1) - 3)/(-4 (u v + 1) (w - 1)^2);   (* 人工协助简化结果 *)
  68. Print["圆O与圆I1连心线长 S1 = ", S1]; Print["圆O与圆I2连心线长 S2 = ", S2];
  69. R1 = Simplify@S[i1, k] ;  R2 = Simplify@S[i2, p] ;  
  70. R1 = ((I (w - 1) + u (w + 1)) (I (w - 1) + v (w + 1)))/((u v +
  71.      1) (w + 1)^2);   (* 人工协助简化结果 *)
  72. R2 = ((u (w - 1) + I (w + 1)) (v (w - 1) + I (w + 1)))/((u v +
  73.      1) (w - 1)^2); (* 人工协助简化结果 *)
  74. Print["I1圆半径 R1 = ", R1]; Print["I2圆半径 R2 = ", R2];
  75. Print["圆O与圆I1连心线长 + 圆I1半径 = ", Factor[Simplify[S1 + R1]]];
  76. Print["圆O与圆I2连心线长 + 圆I2半径 = ", Factor[Simplify[S2 + R2]]];
  77. Print["圆O半径 = ", R];
  78. If[Factor[Simplify[S1 + R1]] == Factor[Simplify[S2 + R2]] == R,
  79. Print["由于圆O与圆I1连心线长+圆I1半径 = 圆O与圆I2连心线长+圆I2半径 = 圆O半径,因此 \
  80. \[CircleDot]I1 和 \[CircleDot]I2 圆都与 \[CircleDot]O 圆相切。"]]
  81. t1 = Simplify[-((R1 Sqrt[ (i1 - o) (
  82. \!\(\*OverscriptBox[\(i1\), \(_\)]\) -
  83. \!\(\*OverscriptBox[\(o\), \(_\)]\))] + i1
  84. \!\(\*OverscriptBox[\(o\), \(_\)]\) - i1
  85. \!\(\*OverscriptBox[\(i1\), \(_\)]\))/(
  86. \!\(\*OverscriptBox[\(i1\), \(_\)]\) -
  87. \!\(\*OverscriptBox[\(o\), \(_\)]\)))];
  88. \!\(\*OverscriptBox[\(t1\), \(_\)]\) = Simplify[(
  89. \!\(\*OverscriptBox[\(i1\), \(_\)]\) (i1 - o) - R1 Sqrt[ (i1 - o) (
  90. \!\(\*OverscriptBox[\(i1\), \(_\)]\) -
  91. \!\(\*OverscriptBox[\(o\), \(_\)]\))])/(i1 - o)];  (*套用公式*)
  92. t1 = (2 (I v u + u + v - I))/(-w + I v (w + 1) + u (v + I) (w + 1) +
  93.   3);
  94. \!\(\*OverscriptBox[\(t1\), \(_\)]\) = (2 (-I v u + u + v + I) w)/(
  95. 3 w - I v (w + 1) + u (v - I) (w + 1) - 1);    (* 人工协助简化结果 *)
  96. Print["t1 = ", t1];
  97. e = Simplify[ (u + v)/2 +
  98.    I ((u^2 v^2 - u^2 - v^2 - 3)/(4 (u v + 1)) - R)];   
  99. \!\(\*OverscriptBox[\(e\), \(_\)]\) =
  100. Simplify[ (u + v)/2 -
  101.    I ((u^2 v^2 - u^2 - v^2 - 3)/(4 (u v + 1)) - R)];
  102. Print["e = ", e];
  103. kT1K = Simplify[kf[t1, k]];  kKE = Simplify[kf[k, e]];
  104. Print["T1K的复斜率 = ", kT1K]; Print["KE的复斜率 = ", kKE];
  105. If[kT1K == kKE, Print["由于T1K的复斜率 = KE的复斜率,所以 T1、K、E 三点共线 "]]
  106. t2 = Simplify[-((R2 Sqrt[ (i2 - o) (
  107. \!\(\*OverscriptBox[\(i2\), \(_\)]\) -
  108. \!\(\*OverscriptBox[\(o\), \(_\)]\))] + i2
  109. \!\(\*OverscriptBox[\(o\), \(_\)]\) - i2
  110. \!\(\*OverscriptBox[\(i2\), \(_\)]\))/(
  111. \!\(\*OverscriptBox[\(i2\), \(_\)]\) -
  112. \!\(\*OverscriptBox[\(o\), \(_\)]\)))];
  113. \!\(\*OverscriptBox[\(t2\), \(_\)]\) = Simplify[(
  114. \!\(\*OverscriptBox[\(i2\), \(_\)]\) (i2 - o) - R2 Sqrt[ (i2 - o) (
  115. \!\(\*OverscriptBox[\(i2\), \(_\)]\) -
  116. \!\(\*OverscriptBox[\(o\), \(_\)]\))])/(i2 - o)];(*套用公式*)  
  117. t2 = -((2 I (u - I) (v - I))/(
  118.   u (v + I) (w - 1) + I v (w - 1) - w - 3));
  119. \!\(\*OverscriptBox[\(t2\), \(_\)]\) = (
  120. 2 (-I v u + u + v + I) w)/(-I v (w - 1) + u (v - I) (w - 1) + 3 w +
  121.   1);  (* 人工协助简化结果 *)
  122. Print["t2 = ", t2];
  123. kEP = Simplify[kf[e, p]];  kPT2 = Simplify[kf[p, t2]];
  124. Print["EP的复斜率 = ", kEP]; Print["PT2的复斜率 = ", kPT2];
  125. If[kT1K == kKE, Print["由于EP的复斜率 = PT2的复斜率,所以 E、P、T2 三点共线 "]]
复制代码


程序运行结果:

运行结果.png

点评

对的。I1I0 / I2I0=(w-1)^2/(w+1)^2, 这个比只与 w 有关。  发表于 2021-12-19 11:47
以上结果表明,I1I:I2I只与w有关  发表于 2021-12-18 23:09
N在外接圆外就不内切了,就是说,这定理不包括这种情形,证明圆交点唯一可以概括。  发表于 2021-12-17 22:08
毋因群疑而阻独见  毋任己意而废人言
毋私小惠而伤大体  毋借公论以快私情
 楼主| 发表于 2021-12-19 20:18:39 | 显示全部楼层
TSC999 发表于 2021-12-17 15:10
下面用楼主的基本方法证明泰博定理。

“人工协助简化结果 ”需要进一步说明,相切判断与下图情况不完全符合。
360截图20211219201457490.jpg
毋因群疑而阻独见  毋任己意而废人言
毋私小惠而伤大体  毋借公论以快私情
您需要登录后才可以回帖 登录 | 欢迎注册

本版积分规则

小黑屋|手机版|数学研发网 ( 苏ICP备07505100号 )

GMT+8, 2022-5-21 23:45 , Processed in 0.184870 second(s), 23 queries .

Powered by Discuz! X3.4

© 2001-2017 Comsenz Inc.

快速回复 返回顶部 返回列表