twitterで次の問題をみかけた。
正方形の対角線に２点${\rm P, Q}$を取り，$∠{\rm POQ}=\frac{\pi}{4}$として，$\overline{\rm AP}=x, \overline{\rm PQ}=z, \overline{\rm QB}=y$ とすると，$x^2+y^2=z^2$が成り立つことを示せ。
Mathematicaでこれを解いてみた。
∠APOと∠OPQ，および，∠BQOと∠OQPに対する余弦定理を等置した式に，△POQに対する余弦定理から得られた式を用いて z を消去する。ただし，PO=√p，QO=√qと置いた。
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
In[1]:= sol = Solve[{(a^2 - x^2 - p)/(2 x Sqrt[p]) == (z^2 + p - q)/(2 z Sqrt[p]),
(a^2 - y^2 - q)/(2 y Sqrt[q]) == (z^2 + q - p)/(2 z Sqrt[q])}, {p, q}]
Out[1]:= {{p -> a^2 - x y - x z, q -> a^2 - x y - y z}}
In[2]:= (z^2 - p - q)^2 == 2 p q /. sol[[1]]
Out[2]= (-2 a^2 + 2 x y + x z + y z + z^2)^2 == 2 (a^2 - x y - x z) (a^2 - x y - y z)
In[3]:= % /. {z -> Sqrt[2] a - x - y}
Out[3]:= (-2 a^2 + x (Sqrt[2] a - x - y) + (Sqrt[2] a - x - y)^2 + 2 x y + (Sqrt[2] a - x - y) y)^2
== 2 (a^2 - x (Sqrt[2] a - x - y) - x y) (a^2 - x y - (Sqrt[2] a - x - y) y)
In[4]:= Simplify[%]
Out[4]:= (a^2 - x y) (a^2 + x y - Sqrt[2] a (x + y)) == 0
In[5]:= z^2 - x^2 - y^2 /. {z -> Sqrt[2] a - x - y} // Simplify
Out[5]:= 2 (a^2 + x y - Sqrt[2] a (x + y))
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
余弦定理を組み合わせて得られた式 Out[4]と三平方の定理からzを消去した式Out[5]は一致したので，問題は解決する。
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
\begin{tikzpicture}
\draw(0,0) rectangle(4,4);
\draw[thin, -] (0,4)--(4,0) node at(-0.15,-0.15){O};
\draw[thin, -] (0,0)--(1.464,2.536) node at(1.64,2.72){P};
\draw[thin, -] (0,0)--(3.155,0.845) node at(3.28,1.02){Q};
\draw(0.20,3.55) circle(0.08) node at(-0.15,4.15){A};
\draw(0.38,0.28) circle(0.08);
\draw(3.55,0.20) circle(0.08) node at(4.15,-0.15){B};
\draw[dotted] (0,4) to [out=335,in=115] (1.464,2.536) node at(1.05,3.5) {$x$};
\draw[dotted] (1.464,2.536) to [out=335,in=115] (3.155,0.845) node at(2.6,1.9) {$z$};
\draw[dotted] (3.155,0.845) to [out=340,in=110] (4,0) node at(3.75,0.7) {$y$};
\draw[dotted] (0,0) to [out=110,in=250] (0,4) node at(-0.2,2) {$a$};
\draw[dotted] (0,0) to [out=340,in=200] (4,0) node at(2,-0.2) {$a$};
\end{tikzpicture}
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
