正方形の対角線に２点P,Qを取り，∠POQ=π4として，¯AP=x,¯PQ=z,¯QB=y とすると，x2+y2=z2が成り立つことを示せ。
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}
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
