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

uk702

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

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

1. ClearAll["Global`*"];
   
2. b={0,0}; a={0,u}; d={v,0}; c={u+v, 0}; (* 令 AB=u, BD=v，则 BC=u+v *)
   
3. 
   
4. (* E 在 AC 上且 DE=DC=u *)
   
5. e = {x, y} /. Simplify@First@Solve[{{x,y} \[Element] InfiniteLine[{a, c}] && EuclideanDistance[{x,y}, d] == u && 0 < x < v}, {x, y}];
   
6. 
   
7. (* 求直线{e, d} 和 直线{b, a} 的交点 *)
   
8. f = {x, y} /. Simplify@First@Solve[Cross[#1 - {x, y}] . (#2 - {x, y}) == 0 & @@@ {{e, d}, {b, a}}, {x, y}];
   
9. 
   
10. lenAfAndFe = (EuclideanDistance[a, f] + EuclideanDistance[f, e]) // Simplify;
    
11. 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 这两个假设已经作为预置条件总是成立的？

uk702

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

1. ClearAll["Global`*"];
   
2. b={0,0}; a={0,u}; d={v,0}; c={u+v, 0}; (* 令 AB=u, BD=v，则 BC=u+v *)
   
3. 
   
4. (* E 在 AC 上且 DE=DC=u *)
   
5. 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}]];
   
6. 
   
7. Print["e = ", e];
   
8. 
   
9. (* 求直线{e, d} 和 直线{b, a} 的交点 *)
   
10. f = {x, y} /. Simplify@First@Solve[Cross[#1 - {x, y}] . (#2 - {x, y}) == 0 & @@@ {{e, d}, {b, a}}, {x, y}];
    
11. Print["f = ", f];
    
12. 
    
13. lenAfAndFe = Assuming[{u > 0, v > 0}, FullSimplify[(EuclideanDistance[a, f] + EuclideanDistance[f, e])]];
    
14. Print["AF+FE = ", lenAfAndFe, " , BD = v，两者当相等"]
    
15. 
    

复制代码

uk702

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

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

复制代码

王守恩

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

\(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\)

姜尧耕_渔樵耕牍

$Assumptions=u>0;

hujunhua

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