# [TYPES] A geometry problem for proof systems

Andrew Myers andru at cs.cornell.edu
Thu Sep 22 08:35:14 EDT 2005

On Thu, Sep 22, 2005 at 06:53:26AM -0400, Peter Freyd wrote:
>
>    angle bisector isosceles
>
>
>    www.mathpages.com/home/kmath433.htm
>
> It has the ugly proof.
>
>    Peter

Here is a more geometric proof:

Theorem:

Given triangle ABC, with angle bisectors BD and EC, angles b = DBC
and c = ECB, show that BD = EC --> ABC is isoceles.

Lemma 1:
Given two triangles ABC and DEF,

If AB = DE & BC = EF, then angle ABC > angle DEF <--> AC > DF

Proof of Lemma 1:

From the law of cosines, we have

AC^2 = AB^2 + BC^2 - 2(AB)(BC)cos(ABC)
DF^2 = DE^2 + EF^2 - 2(DE)(EF)cos(DEF)
= AB^2 + BC^2 - 2(AB)(BC)cos(DEF)

Now,  ABC > DEF <--> cos(ABC) < cos(DEF) <--> AC^2 > DF^2 <--> AC > DF.

Proof of Theorem:
Assume that b > c.

1. Apply Lemma 1 to trangles DBC and ECB, showing that DC > EB.
2. Construct point F such that BEFD is a parallelogram, EF = BD &
EB = DF.
3. Since EF = BD = EC, triangle EFC is isoceles and EFC = ECF.
4. Therefore EFD + DFC = DCE + DCF.
5. EFD = EBD = b > c = DCE, so EFD > DCE and DFC < DCF.
6. By Lemma 1 using DFC and DCF, we have DC < DF = BE, which contradicts
step 1.

Therefore b <= c. Symmetrically, c <= b, so b = c, ABC = ACB,
and ABC is isoceles.

--
Andrew Myers
Associate Professor
Computer Science Department
Cornell University