论坛 › 数学欣赏 › 四条验证i机器证明的高难度定理

dlsh 发表于 2021-12-12 21:35:12

四条验证i机器证明的高难度定理

1五圆定理 2莫利定理3Lemoine 圆定理4,泰博定理

dlsh 发表于 2021-12-14 20:15:15

本帖最后由 dlsh 于 2021-12-14 20:18 编辑

五圆定理证明

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

Clear["Global`*"]

\!\(\*OverscriptBox["a", "_"]\) = 1/a;
\!\(\*OverscriptBox["b", "_"]\) = 1/b;
\!\(\*OverscriptBox["c", "_"]\) = 1/c; g = (a + b + c)/3;
\!\(\*OverscriptBox["g", "_"]\) = (
\!\(\*OverscriptBox["a", "_"]\) +
\!\(\*OverscriptBox["b", "_"]\) +
\!\(\*OverscriptBox["c", "_"]\))/3;
k := (a - b)/(
\!\(\*OverscriptBox["a", "_"]\) -
\!\(\*OverscriptBox["b", "_"]\));
\!\(\*OverscriptBox["k", "_"]\) := 1/k;(*复斜率定义*)
k1 = (a^2 b c)/k; k2 = (b^2 a c)/k;

\!\(\*OverscriptBox["Jd", "_"]\) := -((a1 - k1
\!\(\*OverscriptBox["a1", "_"]\) - (a2 - k2
\!\(\*OverscriptBox["a2", "_"]\)))/(
k1 - k2));(*复斜率等于k1,过点A1与复斜率等于k2,过点A2的直线交点*)
Jd := -((k2 (a1 - k1
\!\(\*OverscriptBox["a1", "_"]\)) - k1 (a2 - k2
\!\(\*OverscriptBox["a2", "_"]\)))/(k1 - k2));
Waixin := (a
\!\(\*OverscriptBox["a", "_"]\) (b - c) + b
\!\(\*OverscriptBox["b", "_"]\) (c - a) + c
\!\(\*OverscriptBox["c", "_"]\) (a - b) )/(
\!\(\*OverscriptBox["a", "_"]\) (b - c) +
\!\(\*OverscriptBox["b", "_"]\) (c - a) +
\!\(\*OverscriptBox["c", "_"]\) (a - b));
\!\(\*OverscriptBox["Waixin", "_"]\) := -((a
\!\(\*OverscriptBox["a", "_"]\) (
\!\(\*OverscriptBox["b", "_"]\) -
\!\(\*OverscriptBox["c", "_"]\)) + b
\!\(\*OverscriptBox["b", "_"]\) (
\!\(\*OverscriptBox["c", "_"]\) -
\!\(\*OverscriptBox["a", "_"]\)) + c
\!\(\*OverscriptBox["c", "_"]\) (
\!\(\*OverscriptBox["a", "_"]\) -
\!\(\*OverscriptBox["b", "_"]\)) )/(
\!\(\*OverscriptBox["a", "_"]\) (b - c) +
\!\(\*OverscriptBox["b", "_"]\) (c - a) +
\!\(\*OverscriptBox["c", "_"]\) (a - b)));
k = Jd;
\!\(\*OverscriptBox["k", "_"]\) =
\!\(\*OverscriptBox["Jd", "_"]\);
L = Jd[-a b, a, -b c, k];
\!\(\*OverscriptBox["L", "_"]\) =
\!\(\*OverscriptBox["Jd", "_"]\)[-a b, a, -b c, k]; t =
Jd[-a b, a, -a c, k];
\!\(\*OverscriptBox["t", "_"]\) =
\!\(\*OverscriptBox["Jd", "_"]\)[-a b, a, -a c, k];
p = Jd[-a b, k, -b c, b];
\!\(\*OverscriptBox["p", "_"]\) =
\!\(\*OverscriptBox["Jd", "_"]\)[-a b, k, -b c, b]; s =
Jd[-c b, b, -a c, k];
\!\(\*OverscriptBox["s", "_"]\) =
\!\(\*OverscriptBox["Jd", "_"]\)[-c b, b, -a c, k];
o1 = Waixin;
\!\(\*OverscriptBox["o1", "_"]\) =
\!\(\*OverscriptBox["Waixin", "_"]\);
Simplify[{k,
\!\(\*OverscriptBox["k", "_"]\)}]
Simplify[{1, t,
\!\(\*OverscriptBox["t", "_"]\), , L,
\!\(\*OverscriptBox[
RowBox[{"L", "\"}], "_"]\), , p,
\!\(\*OverscriptBox["p", "_"]\), , s,
\!\(\*OverscriptBox["s", "_"]\)}]
Simplify[{2, o1,
\!\(\*OverscriptBox["o1", "_"]\), , (o1 - t) (
\!\(\*OverscriptBox["o1", "_"]\) -
\!\(\*OverscriptBox["t", "_"]\))}]
Factor[{2, o1,
\!\(\*OverscriptBox["o1", "_"]\), , (o1 - t) (
\!\(\*OverscriptBox["o1", "_"]\) -
\!\(\*OverscriptBox["t", "_"]\))}]
Simplify[{3, t - L, s - p, , (t - L)/(s - p)}]

TSC999 发表于 2021-12-17 15:10:55

本帖最后由 TSC999 于 2021-12-17 16:40 编辑

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





Clear["Global`*"];(*三个自由变量 u,v,w，其中 w^2 是 CN 的复斜率 *)
i0 = 0;
\!\(\*OverscriptBox[\(i0\), \(_\)]\) = 0;(*三角形ABC的内切圆为单位圆，I0 为内心*)
a = u - I; b = v - I;
\!\(\*OverscriptBox[\(a\), \(_\)]\) = u + I;
\!\(\*OverscriptBox[\(b\), \(_\)]\) = v + I;
c = ((u + v) + I (v u - 1))/(u v + 1);
\!\(\*OverscriptBox[\(c\), \(_\)]\) = ((u + v) - I (v u - 1))/(
u v + 1);(*采用已知公式：三角形ABC的C点复坐标*)Print["c = ", c];
o = ((u - I) (v - I) (I v u + u + v + 3 I))/(4 (u v + 1));
\!\(\*OverscriptBox[\(o\), \(_\)]\) = ((u + I) (v + I) (-I u v + u +
    v - 3 I))/(
4 (u v + 1)); (* 采用已知公式：三角形ABC的外接圆圆心O点复坐标*) Print["o = ", o];
R = -(((1 + u^2) (1 + v^2))/(
4 (1 + u v)));(* 采用已知公式：三角形ABC外接圆的半径 R *)Print["外接圆半径 R = ", R];
kf := (a - b)/(
\!\(\*OverscriptBox[\(a\), \(_\)]\) -
\!\(\*OverscriptBox[\(b\), \(_\)]\));
\!\(\*OverscriptBox[\(kf\), \(_\)]\) :=
1/kf; (* AB 直线的复斜率 *)
(* 以下求角ANC平分线 m 的复斜率, 由于AB的复斜率 kab=1，CN的复斜率 knc=w^2, 所以角平分线的复斜率 km=w\
*)
(* 角ANB平分线 n 与 m 垂直，所以直线 n 的复斜率=-w。另外因直线 KI0//n，故 KI0的复斜率也等于 -w *)
km = w; kn = -w; kcn = w^2;
Jd := -((k2 (a1 - k1
\!\(\*OverscriptBox[\(a1\), \(_\)]\)) - k1 (a2 - k2
\!\(\*OverscriptBox[\(a2\), \(_\)]\)))/(k1 - k2));

\!\(\*OverscriptBox[\(Jd\), \(_\)]\) := -((a1 - k1
\!\(\*OverscriptBox[\(a1\), \(_\)]\) - (a2 - k2
\!\(\*OverscriptBox[\(a2\), \(_\)]\)))/(
      k1 - k2)); (*复斜率等于k1,过点A1与复斜率等于k2,过点A2的直线交点*)
n = Simplify@ Jd;
\!\(\*OverscriptBox[\(n\), \(_\)]\) = Simplify@
\!\(\*OverscriptBox[\(Jd\), \(_\)]\); Print["n = ", n];
k = Simplify@ Jd;
\!\(\*OverscriptBox[\(k\), \(_\)]\) = Simplify@
\!\(\*OverscriptBox[\(Jd\), \(_\)]\); Print["k = ", k];
p = Simplify@ Jd;
\!\(\*OverscriptBox[\(p\), \(_\)]\) = Simplify@
\!\(\*OverscriptBox[\(Jd\), \(_\)]\); Print["p = ", p];
(* 以下求 I1 点的复坐标。它是两直线的交点，一条是复斜率为-1、经过K点的线，另一条是复斜率为 km、经过N点的线 *)
i1 = Simplify@ Jd[-1, k, km, n];
\!\(\*OverscriptBox[\(i1\), \(_\)]\) = Simplify@
\!\(\*OverscriptBox[\(Jd\), \(_\)]\)[-1, k, km,
   n]; Print["i1 = ", i1];
(* 以下求 I2 点的复坐标。它是两直线的交点，一条是复斜率为-1、经过P点的线，另一条是复斜率为 kn、经过N点的线 *)
i2 = Simplify@ Jd[-1, p, kn, n];
\!\(\*OverscriptBox[\(i2\), \(_\)]\) = Simplify@
\!\(\*OverscriptBox[\(Jd\), \(_\)]\)[-1, p, kn, n]; Print["i2 = ", i2];
ki1i0 = Simplify];
ki0i2 = Simplify]; (* 证明 I1、I0、I2 三点共线 *)
Print["I1I0的复斜率 =", ki1i0]; Print["I0I2的复斜率 =", ki0i2];
If[ki1i0 == ki0i2,
Print["由于 I1I0 的复斜率等于 I0I2 的复斜率，所以 I1、I0、I2 三点共线。"]];
S := Sqrt[(a - b) (
\!\(\*OverscriptBox[\(a\), \(_\)]\) -
\!\(\*OverscriptBox[\(b\), \(_\)]\))];(* A、B 点间的距离 *)
(* 以I1为圆心、I1K为半径作圆I1; 以I2为圆心、I2P为半径作圆I2，则两圆都与BC和CN相切 *)
(* 以下证明I1圆和I2圆都与O圆相内切 *)
S1 = Simplify@S;   (* I1圆和O圆连心线长度，未简化 *)
S2 = Simplify@S ; (* I2圆和O圆连心线长度，未简化 *)
S1 = (-3 w^2 + 10 w + v^2 (w + 1)^2 + u^2 (v^2 + 1) (w + 1)^2 +
   4 I v (w^2 - 1) + 4 u (w + 1) (I (w - 1) + v (w + 1)) -
   3)/(-4 (u v + 1) (w + 1)^2); (* 人工协助简化结果 *)
S2 = (v^2 (w - 1)^2 + u^2 (v^2 + 1) (w - 1)^2 +
   4 u (v (w - 1) + I (w + 1)) (w - 1) - 3 w^2 - 10 w +
   4 I v (w^2 - 1) - 3)/(-4 (u v + 1) (w - 1)^2);   (* 人工协助简化结果 *)
Print["圆O与圆I1连心线长 S1 = ", S1]; Print["圆O与圆I2连心线长 S2 = ", S2];
R1 = Simplify@S ;R2 = Simplify@S ;
R1 = ((I (w - 1) + u (w + 1)) (I (w - 1) + v (w + 1)))/((u v +
   1) (w + 1)^2);   (* 人工协助简化结果 *)
R2 = ((u (w - 1) + I (w + 1)) (v (w - 1) + I (w + 1)))/((u v +
   1) (w - 1)^2); (* 人工协助简化结果 *)
Print["I1圆半径 R1 = ", R1]; Print["I2圆半径 R2 = ", R2];
Print["圆O与圆I1连心线长 + 圆I1半径 = ", Factor]];
Print["圆O与圆I2连心线长 + 圆I2半径 = ", Factor]];
Print["圆O半径 = ", R];
If] == Factor] == R,
Print["由于圆O与圆I1连心线长+圆I1半径 = 圆O与圆I2连心线长+圆I2半径 = 圆O半径，因此 \
\I1 和 \I2 圆都与 \O 圆相切。"]]
t1 = Simplify[-((R1 Sqrt[ (i1 - o) (
\!\(\*OverscriptBox[\(i1\), \(_\)]\) -
\!\(\*OverscriptBox[\(o\), \(_\)]\))] + i1
\!\(\*OverscriptBox[\(o\), \(_\)]\) - i1
\!\(\*OverscriptBox[\(i1\), \(_\)]\))/(
\!\(\*OverscriptBox[\(i1\), \(_\)]\) -
\!\(\*OverscriptBox[\(o\), \(_\)]\)))];
\!\(\*OverscriptBox[\(t1\), \(_\)]\) = Simplify[(
\!\(\*OverscriptBox[\(i1\), \(_\)]\) (i1 - o) - R1 Sqrt[ (i1 - o) (
\!\(\*OverscriptBox[\(i1\), \(_\)]\) -
\!\(\*OverscriptBox[\(o\), \(_\)]\))])/(i1 - o)];(*套用公式*)
t1 = (2 (I v u + u + v - I))/(-w + I v (w + 1) + u (v + I) (w + 1) +
3);
\!\(\*OverscriptBox[\(t1\), \(_\)]\) = (2 (-I v u + u + v + I) w)/(
3 w - I v (w + 1) + u (v - I) (w + 1) - 1);    (* 人工协助简化结果 *)
Print["t1 = ", t1];
e = Simplify[ (u + v)/2 +
   I ((u^2 v^2 - u^2 - v^2 - 3)/(4 (u v + 1)) - R)];   
\!\(\*OverscriptBox[\(e\), \(_\)]\) =
Simplify[ (u + v)/2 -
   I ((u^2 v^2 - u^2 - v^2 - 3)/(4 (u v + 1)) - R)];
Print["e = ", e];
kT1K = Simplify];kKE = Simplify];
Print["T1K的复斜率 = ", kT1K]; Print["KE的复斜率 = ", kKE];
If]
t2 = Simplify[-((R2 Sqrt[ (i2 - o) (
\!\(\*OverscriptBox[\(i2\), \(_\)]\) -
\!\(\*OverscriptBox[\(o\), \(_\)]\))] + i2
\!\(\*OverscriptBox[\(o\), \(_\)]\) - i2
\!\(\*OverscriptBox[\(i2\), \(_\)]\))/(
\!\(\*OverscriptBox[\(i2\), \(_\)]\) -
\!\(\*OverscriptBox[\(o\), \(_\)]\)))];
\!\(\*OverscriptBox[\(t2\), \(_\)]\) = Simplify[(
\!\(\*OverscriptBox[\(i2\), \(_\)]\) (i2 - o) - R2 Sqrt[ (i2 - o) (
\!\(\*OverscriptBox[\(i2\), \(_\)]\) -
\!\(\*OverscriptBox[\(o\), \(_\)]\))])/(i2 - o)];(*套用公式*)
t2 = -((2 I (u - I) (v - I))/(
u (v + I) (w - 1) + I v (w - 1) - w - 3));
\!\(\*OverscriptBox[\(t2\), \(_\)]\) = (
2 (-I v u + u + v + I) w)/(-I v (w - 1) + u (v - I) (w - 1) + 3 w +
1);(* 人工协助简化结果 *)
Print["t2 = ", t2];
kEP = Simplify];kPT2 = Simplify];
Print["EP的复斜率 = ", kEP]; Print["PT2的复斜率 = ", kPT2];
If]


程序运行结果：

dlsh 发表于 2021-12-19 20:18:39

TSC999 发表于 2021-12-17 15:10
下面用楼主的基本方法证明泰博定理。




“人工协助简化结果 ”需要进一步说明，相切判断与下图情况不完全符合。

查看完整版本: 四条验证i机器证明的高难度定理