BD,CE 是 ΔABC 的角平分线，DE 与 ΔABC 外接圆交于 F ，证明 1／FB=1／FC+1／FA

creasson

creasson 发表于 2023-4-10 10:20
对于这种对点的位置有要求的命题， 纯粹地用单位复数表示是困难的，并不能准确区分应取哪个根.  而当直接求 ...

对于\(\triangle{BCF}\), 它的一个表示是
\[\mathop {BF}\limits^ \to   = \frac{{1 + i\cot \angle BFC}}{{1 - i\cot \angle BCF}}\mathop {BC}\limits^ \to  \]
这里的\(u\)即是\(\cot \angle BCF\), 而
\[\cot \angle BFC = \cot \angle BAC = \frac{{1 - {s^2}}}{{2s}}\]
这些是形式上的，不必细究.  事实上，也可以用任意其他的参数表示， 例如，根据\(A,B,C,F\)四点的交比为实数， 可设
\[\frac{{F - A}}{{F - B}}\frac{{C - B}}{{C - A}} = v\]

王守恩

\(记BC=\sin(2A),CA=\sin(2B),AB=\sin(2C),∠BAF=∠BCF=x\)

\(已知:\frac{AB*b}{BC*c+CA*a}=\frac{\sin(2C)*\sin(2A+x)}{\sin(2A)*\sin(2C-x)+\sin(2B)*\sin(x)}=1\)

\(求:k=\frac{1/a}{1/b+1/c}=\frac{1/\sin(x)}{1/\sin(2A+x)+1/\sin(2C-x)}=1\)

\(\sin(2A),\sin(2B),\sin(2C),\sin(x),\sin(2A+x),\sin(2C-x)都是长度单位。\)

下面4个算式都在说：x 有唯一的答案。

1,\(\frac{\sin(2C)*\sin(2A+x)}{\sin(2A)*\sin(2C-x)+\sin(2B)*\sin(x)}=\frac{1/\sin(x)}{1/\sin(2A+x)+1/\sin(2C-x)}=k\)

2,\(\frac{\sin(2C)*\sin(2A+x)}{\sin(2A)*\sin(2C-x)+\sin(2B)*\sin(x)}=\frac{1/\sin(x)}{1/\sin(2A+x)+1/\sin(2C-x)}=1\)

3,\(\frac{\sin(2C)*\sin(2A+x)}{\sin(2A)*\sin(2C-x)+\sin(2B)*\sin(x)}=\frac{1/\sin(x)}{1/\sin(2A+x)+1/\sin(2C-x)}\)

4,\(\frac{\sin(2C)*\sin(2A+x)}{\sin(2A)*\sin(2C-x)+\sin(2B)*\sin(x)}=k\ \ \ \frac{1/\sin(x)}{1/\sin(2A+x)+1/\sin(2C-x)}=1\)

天山草

以上是用三角形 ABC 的三边长度 \(a，b，c\) 来表示 \(x，y，z，x1，y1，z1\)。

这个公式是【悠闲数学娱乐论坛】的 hejoseph 用重心坐标法算出来的。

uk702

天山草 发表于 2023-4-10 19:32
以上是用三角形 ABC 的三边长度 \(a，b，c\) 来表示 \(x，y，x1，y1\)。

这个公式是【悠闲数学娱乐 ...

另一个思路，首先我们根据托勒密定理及一个余弦公式，发现这时 {x, y, z } 三个参数只能解出两个，这是显然的，毕竟没有用到 FED 共线，甚至也没有用到 D、E 是角平分线。

这时我们将 1/x == 1/y + 1/z 作为已知加入去求解方程，解出的 {x,y,z}，如果跟我们已知的公式相符，题主的问题就可得证。



和 #13 对照了一下，分母应该是相同的，分子是否相同，肉眼暂时看不出来。
分子中的 Sqrt[a^2 + (b - c)^2 + 2 a (b + c)])  和 #13 楼也是相一致的，还真有可能经过最终化简证明两个公式相互是一致的。

天山草

下面是根据  8#楼 creasson 大侠所写程序的简化版，可供各位研究其中的奥妙。

运行结果：


F 点的表达式来源，见 11# 楼 creasson 的说明。

1. Clear["Global`*"]; (*令 s=tanA/2, t=tanB/2, u=1/tan\[Angle]BAC*)
   
2. Print["根据构图，可直接引用此构图下的各点坐标如下(但 F 点的坐标最终尚取决于参变数 u 的取值)： "];
   
3. points = {B -> 0, C -> 1, A -> ((s + t) (1 - s t))/(s (1 - I t)^2),   pI -> (1 - s t)/(1 - I t),   D -> (2 I (s^2 t + s (t^2 - 1) - t))/((t + I) (s^2 t - 2 s - t)),   pE -> ((t - I) (s t - 1))/((t + I) (s t + 1)),   F -> (1 + I*(1 - s^2)/(2 s))/(1 - I u)}(*pI是内心的表示*)(*取值范围限定*)
   
4. cond = s > 0 && t > 0 && 1 - s t > 0;
   
5. (*根据D,E,F共线得到u的方程：*)
   
6. uEQ = (Factor[ComplexExpand[Im[#]]] // Numerator) &@((D - F)/(D - pE) /. points);(*因D,E,F共线所以该式虚部的分子为零*)
   
7. Print["参数 u 应满足以下方程: "];
   
8. Print[uEQ, " = 0  -------①"];
   
9. Print["根据 F 点的位置确定参数 s、t、u 的取值范围如下: "];
   
10. cond = Reduce[Factor[ComplexExpand[Im[(F - B)/(A - B) /. points]]] > 0 &&  cond, {s, t, u}]
    
11. (*计算 FA,FB,FC的长度*)
    
12. Print["FA、FB、FC 的长度: "];
    
13. dists = FullSimplify[ComplexExpand[Abs[#]], Assumptions -> cond] & /@ ({F - A, F - B, F - C} /. points);
    
14. {FA -> dists[[1]], FB -> dists[[2]], FC -> dists[[3]]}
    
15. target = (1/dists[[2]] - 1/dists[[1]] - 1/dists[[3]]) // Factor;
    
16. Print["如果能证明下面这个式子等于零，则完成证明: "];
    
17. Print[target, "   -------②"];
    
18. Print["因为 ① 式等于零，而 ① 式的前两个因式不等于零，故第三个因式应为零。② 式分子中也有这个因式，所以 ② 式必为零，故命题 1/FB - 1/FA -1/FC = 0 成立。"]

复制代码

Ysu2008

能不能用人工智能搞一下？

uk702

@天山草

只要能证明 #13 楼的公式是正确的，并且 #14楼给出的公式和 #13 相一致，应该就算给出了证明。说白了，#13 给出 {x,y,z} 的计算公式，#14 给出了如果 1/x=1/y+1/z 成立  {x,y,z} 应满足的条件。

这样，如果 #14 的结果跟 #13 相一致，就表明 #13 给出的公式满足 1/x=1/y+1/z，如果不相一致，并且 MMA 没有漏解，则必然有 1/x != 1/y + 1/z。


应该可以确认 #13 给出的公式和 #14 相一致。

```
sol = Solve[{x b + y a == z c, (z^2 + a^2 - x^2) / (z a) == (y^2 + c^2 - x^2) / (y c), 1/x == 1/y + 1/z}, {x, y, z}];
x = x /. sol[[1]]; FullSimplify[x^2]
```

输出：

\[
\frac{a c \left(a^3+a^2 \left(\sqrt{2 c (a-b)+(a+b)^2+c^2}+2 b+c\right)+a \left(b \left(\sqrt{2 c (a-b)+(a+b)^2+c^2}+2 c\right)+b^2-c^2\right)+c (b-c) \left(\sqrt{2 c (a-b)+(a+b)^2+c^2}-b+c\right)\right)}{2 \left(a^3+a^2 (b+c)-a \left(b^2-3 b c+c^2\right)-(b-c)^2 (b+c)\right)}
\]

天山草

@uk702:
我的 MMA 版本是 9.0 的，版本低，没有你那个好用。输出的结果化简不彻底?



再看看，好像跟你 14# 楼的结果是一样的？

你的 MMA 版本是多少的？

天山草

13# 楼的公式又增加了 \(z\) 和  \(z1\) 的公式。但是直接用这些公式借助 mathematica 来证明主帖中的命题，初步试了试是行不通的，因为 MMA 在处理带有根式的公式时能力有限。用这些公式通过人工变换的方法倒是有可能解决问题。

@uk702:  你在 17# 楼的解方程中用 FullSimplify[sol[[1]]] 是增根，要把 1 改为 4 才对，即改为 FullSimplify[sol[[4]]] 就对了，而FullSimplify[sol[[3]]] 等于负的 FullSimplify[sol[[4]]]。当然 FullSimplify[sol[[3]]] 也是增根。
FullSimplify[sol[[2]]] 也是增根。
用人工变换 FullSimplify[sol[[4]]] 给出的公式，能得到与 13# 楼中的 \(z\) 完全相同的结果。

人工变换过程如下：


uk702 在 17#楼的解方程方法是有用的，如果事先不知道 13# 楼的那些公式，如何判断哪个是增根？最好的办法是先画一个图，量出有关线段的长度，再以此检验哪个是增根。

王守恩

一个有趣的现象(1楼的图)：∠EAF=x, ∠EFA=y, x+y=k可以是整数角度。

Table[NSolve[{(Sin[2C\[Pi]/180]Sin[(2A+x)\[Pi]/180])/(Sin[2A\[Pi]/180]Sin[(2C-x)\[Pi]/180]
+ Sin[2 B \[Pi]/180] Sin[x \[Pi]/180]) == (1/Sin[x \[Pi]/180])/(1/Sin[(2 A + x) \[Pi]/180]
+ 1/Sin[(2 C - x) \[Pi]/180]), (Sin[(2 A + B) \[Pi]/180] Sin[(2 B + C - x - y) \[Pi]/180])/(
Sin[(x + y - B) \[Pi]/180] Sin[(2 B + C) \[Pi]/180]) == 1,  x + y == k,
90 > x > 0, 90 > y >0}, {x, y, k}], {A, 1, 30}, {B, 45 - A/2, 45 - A/2}, {C, 90 - A - B, 90 - A - B}]

{{{{x -> 9.62908, y -> 79.3709, k -> 89.}}}}, {{{{x -> 12.9307, y -> 75.0693, k -> 88.}}}},
{{{{x -> 15.1691, y -> 71.8309, k -> 87.}}}}, {{{{x -> 16.8518, y -> 69.1482, k -> 86.}}}},
{{{{x -> 18.1775, y -> 66.8225, k -> 85.}}}}, {{{{x -> 19.2489, y -> 64.7511, k -> 84.}}}},
{{{{x -> 20.1277, y -> 62.8723, k -> 83.}}}}, {{{{x -> 20.8546, y -> 61.1454, k -> 82.}}}},
{{{{x -> 21.4577, y -> 59.5423, k -> 81.}}}}, {{{{x -> 21.9579, y -> 58.0421, k -> 80.}}}},
{{{{x -> 22.3709, y -> 56.6291, k -> 79.}}}}, {{{{x -> 22.7092, y -> 55.2908, k -> 78.}}}},
{{{{x -> 22.9824, y -> 54.0176, k -> 77.}}}}, {{{{x -> 23.1986, y -> 52.8014, k -> 76.}}}},
{{{{x -> 23.3644, y -> 51.6356, k -> 75.}}}}, {{{{x -> 23.4854, y -> 50.5146, k -> 74.}}}},
{{{{x -> 23.5661, y -> 49.4339, k -> 73.}}}}, {{{{x -> 23.6107, y -> 48.3893, k -> 72.}}}},
{{{{x -> 23.6224, y -> 47.3776, k -> 71.}}}}, {{{{x -> 23.6044, y -> 46.3956, k -> 70.}}}},
{{{{x -> 23.5593, y -> 45.4407, k -> 69.}}}}, {{{{x -> 23.4893, y -> 44.5107, k -> 68.}}}},
{{{{x -> 23.3965, y -> 43.6035, k -> 67.}}}}, {{{{x -> 23.2826, y -> 42.7174, k -> 66.}}}},
{{{{x -> 23.1494, y -> 41.8506, k -> 65.}}}}, {{{{x -> 22.9983, y -> 41.0017, k -> 64.}}}},
{{{{x -> 22.8305, y -> 40.1695, k -> 63.}}}}, {{{{x -> 22.6473, y -> 39.3527, k -> 62.}}}},
{{{{x -> 22.4497, y -> 38.5503, k -> 61.}}}}, {{{{x -> 22.2388, y -> 37.7612, k -> 60.}}}}}