本帖最后由 hbghlyj 于 2020-5-13 13:44 编辑 尝试把一类线段乘积恒等式的证明过程形式化。欢迎提出更好的方法！
其通式为$A_1B_1\cdot A_2B_2\cdot\cdots\cdot A_nB_n=C_1D_1\cdot C_2D_2\cdot\cdots\cdot C_nD_n$
把它对应为线性方程组$i_{a_1,b_1}+i_{a_2,b_2}\cdot\cdots\cdot i_{a_n,b_n}=i_{c_1,d_1}+i_{c_2,d_2}+\cdots+i_{c_n,d_n}$
并约定$i_{a,b}=i_{b,a}$
一、平行线截线段成比例
我们不会用到AB+BC=AC这样的线段恒等式(因为它出现了线段的和)，这意味着，“ABC,ADE共线，BC∥DE"需表示为三个等式- px[a_, b_, c_, d_,
- e_] = {Subscript[i, a, b] - Subscript[i, a, d] ==
- Subscript[i, a, c] - Subscript[i, a, e],
- Subscript[i, b, d] - Subscript[i, a, d] ==
- Subscript[i, c, e] - Subscript[i, a, e],
- Subscript[i, a, b] - Subscript[i, a, d] ==
- Subscript[i, b, c] - Subscript[i, d, e]}
和上面类似的理由，(a,b;c,d)=(e,f;g,h)需表示为两个等式- cd[a_, b_, c_, d_, e_, f_, g_,
- h_] = {Subscript[i, a, b] - Subscript[i, a, d] - Subscript[i, b,
- c] + Subscript[i, c, d] ==
- Subscript[i, e, f] - Subscript[i, e, h] - Subscript[i, f, g] +
- Subscript[i, g, h],
- Subscript[i, a, c] + Subscript[i, b, d] - Subscript[i, a, d] -
- Subscript[i, b, c] ==
- Subscript[i, e, g] + Subscript[i, f, h] - Subscript[i, e, h] -
- Subscript[i, f, g]};
- blb[{a_, b_}] = Subscript[i, a, b]
- list = blb /@ Subsets[{a, b, c, d, e, f, g, h, k, j}, {2}]
- blb2[{a_, b_}] = Subscript[i, b, a] -> Subscript[i, a, b]
- list2 = blb2 /@ Subsets[{a, b, c, d, e, f, g, h, k, j}, {2}]
- eq = Join[cd[a, b, c, d, f, g, h, k], cd[a, b, c, e, f, g, h, j],
- cd[a, b, d, e, f, g, k, j], cd[a, c, d, e, f, h, k, j],
- cd[b, c, d, e, g, h, k, j]] /. list2
- Reduce[eq, list]
- Subscript[i, g, k] ==
- Subscript[i, a, c] - Subscript[i, a, d] - Subscript[i, b, c] +
- Subscript[i, b, d] - Subscript[i, f, h] + Subscript[i, f, k] +
- Subscript[i, g, h] &&
- Subscript[i, g, j] ==
- Subscript[i, a, c] - Subscript[i, a, e] - Subscript[i, b, c] +
- Subscript[i, b, e] - Subscript[i, f, h] + Subscript[i, f, j] +
- Subscript[i, g, h] &&
- Subscript[i, h, k] ==
- Subscript[i, a, b] - Subscript[i, a, d] - Subscript[i, b, c] +
- Subscript[i, c, d] - Subscript[i, f, g] + Subscript[i, f, k] +
- Subscript[i, g, h] &&
- Subscript[i, h, j] ==
- Subscript[i, a, b] - Subscript[i, a, e] - Subscript[i, b, c] +
- Subscript[i, c, e] - Subscript[i, f, g] + Subscript[i, f, j] +
- Subscript[i, g, h] &&
- Subscript[i, k, j] ==
- Subscript[i, a, b] + Subscript[i, a, c] - Subscript[i, a, d] -
- Subscript[i, a, e] - Subscript[i, b, c] + Subscript[i, d, e] -
- Subscript[i, f, g] - Subscript[i, f, h] + Subscript[i, f, j] +
- Subscript[i, f, k] + Subscript[i, g, h]
- cd[a_, b_, c_, d_, e_, f_, g_, h_, k_,
- j_] = {Subscript[i, g, k] ==
- Subscript[i, a, c] - Subscript[i, a, d] - Subscript[i, b, c] +
- Subscript[i, b, d] - Subscript[i, f, h] + Subscript[i, f, k] +
- Subscript[i, g, h],
- Subscript[i, g, j] ==
- Subscript[i, a, c] - Subscript[i, a, e] - Subscript[i, b, c] +
- Subscript[i, b, e] - Subscript[i, f, h] + Subscript[i, f, j] +
- Subscript[i, g, h],
- Subscript[i, h, k] ==
- Subscript[i, a, b] - Subscript[i, a, d] - Subscript[i, b, c] +
- Subscript[i, c, d] - Subscript[i, f, g] + Subscript[i, f, k] +
- Subscript[i, g, h],
- Subscript[i, h, j] ==
- Subscript[i, a, b] - Subscript[i, a, e] - Subscript[i, b, c] +
- Subscript[i, c, e] - Subscript[i, f, g] + Subscript[i, f, j] +
- Subscript[i, g, h],
- Subscript[i, k, j] ==
- Subscript[i, a, b] + Subscript[i, a, c] - Subscript[i, a, d] -
- Subscript[i, a, e] - Subscript[i, b, c] + Subscript[i, d, e] -
- Subscript[i, f, g] - Subscript[i, f, h] + Subscript[i, f, j] +
- Subscript[i, f, k] + Subscript[i, g, h]}
|
