三平方の定理（１）

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}

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -