[TYPES] A geometry problem for proof systems

[Andrew Myers]

On Thu, Sep 22, 2005 at 06:53:26AM -0400, Peter Freyd wrote:
> These days, of course, one just asks Google. The query:
> 
>    angle bisector isosceles
> 
> leads one to 
> 
>    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