MMA 中，如何指定某些假设（条件）成立？

公子相

如下的一道几何题：
Rt△ABC 中，∠ABC=90°，直线 l 交 BC、CA 及 BA 的延长线于 D、E、F，若 DE=DC=AB，求证：AF+EF=BD。

以下的 MMA 代码是对问题的简单 “直译”：

1. ClearAll["Global`*"];b={0,0}; a={0,u}; d={v,0}; c={u+v, 0}; (* 令 AB=u, BD=v，则 BC=u+v *)(* E 在 AC 上且 DE=DC=u *)e = {x, y} /. Simplify@First@Solve[{{x,y} \[Element] InfiniteLine[{a, c}] && EuclideanDistance[{x,y}, d] == u && 0 < x < v}, {x, y}];(* 求直线{e, d} 和 直线{b, a} 的交点 *)f = {x, y} /. Simplify@First@Solve[Cross[#1 - {x, y}] . (#2 - {x, y}) == 0 & @@@ {{e, d}, {b, a}}, {x, y}];lenAfAndFe = (EuclideanDistance[a, f] + EuclideanDistance[f, e]) // Simplify;Print["AF+FE = ", lenAfAndFe, " , BD = v，两者当相等"]

复制代码

结果显示：

AF+FE = v if u>0&&v>0 , BD = v，两者当相等

故命题得证。

其中，求解 E  有坐标时，MMA 返回
\( \left\{\fbox{$\frac{v^2 (u+v)}{2 u^2+2 v u+v^2}\text{ if }u>0\land v>0$},\fbox{$\frac{2 u^2 (u+v)}{2 u^2+2 v u+v^2}\text{ if }u>0\land v>0$}\right\} \)

求助各位专家，不知是否有办法让 MMA 知道 u>0 和 v>0 这两个假设已经作为预置条件总是成立的？

erawaliktevi

经实验将代码改为如下可行，求大佬们提供更好的写法（多处都要加 Assuming[{u > 0, v > 0}, xxx] 挺烦人的）：

1. ClearAll["Global`*"];b={0,0}; a={0,u}; d={v,0}; c={u+v, 0}; (* 令 AB=u, BD=v，则 BC=u+v *)(* E 在 AC 上且 DE=DC=u *)e = {x, y} /. Simplify@First@Assuming[{u > 0, v > 0}, Solve[{{x,y} \[Element] InfiniteLine[{a, c}] && EuclideanDistance[{x,y}, d] == u && 0 < x < v}, {x, y}]];Print["e = ", e]; (* 求直线{e, d} 和 直线{b, a} 的交点 *)f = {x, y} /. Simplify@First@Solve[Cross[#1 - {x, y}] . (#2 - {x, y}) == 0 & @@@ {{e, d}, {b, a}}, {x, y}];Print["f = ", f];lenAfAndFe = Assuming[{u > 0, v > 0}, FullSimplify[(EuclideanDistance[a, f] + EuclideanDistance[f, e])]];Print["AF+FE = ", lenAfAndFe, " , BD = v，两者当相等"]

复制代码

erileiyuqig

经实验，可以将 Assuming[{u > 0, v > 0} 放到最外层，让整个代码都包裹进这个假设里，这样就可以避免多处重复写这段代码：

1. ```ClearAll["Global`*"];Assuming[{u > 0, v > 0},        b={0,0}; a={0,u}; d={v,0}; c={u+v, 0}; (* 令 AB=u, BD=v，则 BC=u+v *)        (* E 在 AC 上且 DE=DC=u *)        e = {x, y} /. Simplify@First@ Solve[{{x,y} \[Element] InfiniteLine[{a, c}] && EuclideanDistance[{x,y}, d] == u && 0 < x < v}, {x, y}];        Print["e = ", e];         (* 求直线{e, d} 和 直线{b, a} 的交点 *)        f = {x, y} /. Simplify@First@Solve[Cross[#1 - {x, y}] . (#2 - {x, y}) == 0 & @@@ {{e, d}, {b, a}}, {x, y}];        Print["f = ", f];        lenAfAndFe = FullSimplify[(EuclideanDistance[a, f] + EuclideanDistance[f, e])];        Print["AF+FE = ", lenAfAndFe, " , BD = v，两者当相等"]]        ```

复制代码

ulenkusefihj

我只会做具体的题目，可以这样(恒等式)。

\(AB=\sin(\theta),BD=\cos(\theta)-\sin(\theta),AE=1-\sin(2\theta)\)

\(\frac{AF+EF}{BD}=\frac{(1-\sin(2\theta))(\cos(\theta)+\sin(\theta))/cos(2\theta)}{\cos(\theta)-\sin(\theta)}=1\)

ouukucakac

$Assumptions=u>0;

DJWilliamstada

CD=AB → Rt△ABD≌Rt△CDG
所以BC=BD-CD=BH-AB=AH=AF+FH=AF+EF