A Computer Algebra Aided Proof in Plane Geometry

Given \Delta ABC and two squares ABEF, ACGH in Fig. 1. The squares are sitting on the two sides of \Delta ABC, AB and AC, respectively. Both squares are oriented away from the interior of \Delta ABC. \Delta BCP is an isosceles right triangle. P is on the same side of A. Prove that points E, P and G lie on the same line.

Fig. 1

Introducing rectangular coordinates show in Fig. 2:

Fig. 2

We observe that


x_1 < -a\quad\quad(2)

x_3 > a\quad\quad\quad(3)

CG=CA\implies (x-a)^2+y_3^2 = (x-a)^2 +y^2\quad\quad(4)

AB=AE\implies (x+a)^2+y^2=(x_1+a)^2+y_1^2\quad\quad(5)

CG\perp CA \implies y_3 y = -(x-a)(x_3-a)\quad\quad\quad(6)

BE\perp AB \implies y_1y = -(x_1+a)(x+a)\quad\quad\quad(7)

Fig. 3

Solving system of equations (4), (5), (6), (7), we obtain four set of solutions:

x_1=-y-a, y_1=x+a, x_3=y+a, y_3=a-x\quad\quad(8)

x_1=y-a, y_1=-x-a, x_3=y+a, y_3=a-x\quad\quad(9)

x_1=-y-a, y_1=x+a, x_3=a-y, y_3=x-a\quad\quad(10)

x_1=y-a, y_1=-x-a, x_3=a-y, y_3=x-a\quad\quad(11)

Among them, only (10) truly represents the coordinates in Fig. 2.

Fig. 4

By Heron’s formula (see “Had Heron Known Analytic Geometry…“), the area of triangle with vortex (-y-a, x+a), (0, a), (y+a, a-x) is

\frac{1}{2}\begin{vmatrix} -y-a & x+a & 1 \\ 0 & a &1 \\ y+a & a-x & 1\end{vmatrix}.

From Fig. 4, we see that it is zero.


E, P, G lie on the same line.

The reason we do not consider (9), (10), (11) is due to the fact that

(9) contradicts (2) since y>0, a>0 \implies x_1=y-a=-a+y>-a.


by (1), (10) and (11) indicate x_3=a-y <a which contradicts (3).

Exercise-1 Prove “E, P, G lie on the same line” with complex numbers (hint: see “Treasure Hunt with Complex Numbers“).


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s