[TYPES] A geometry problem for proof systems
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:
> These days, of course, one just asks Google. The query:
> angle bisector isosceles
> leads one to
> It has the ugly proof.
Here is a more geometric proof:
Given triangle ABC, with angle bisectors BD and EC, angles b = DBC
and c = ECB, show that BD = EC --> ABC is isoceles.
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
Therefore b <= c. Symmetrically, c <= b, so b = c, ABC = ACB,
and ABC is isoceles.
Computer Science Department
More information about the Types-list