Erdős-Mordell Theorem

Author

Eric W. Weisstein
December 30, 2003

This notebook downloaded from http://mathworld.wolfram.com/notebooks/PlaneGeometry/Erdos-MordellTheorem.nb.

For more information, see Eric's MathWorld entry http://mathworld.wolfram.com/Erdos-MordellTheorem.html.

©2005 Wolfram Research, Inc. except for portions noted otherwise

Figure

t=Triangle[{{0,0},{1,0},{.4,.7}}];
p=Centroid[t];
Show[Graphics[{
t,
{Red,
PedalLines[t,p],
PerpSquare[#,.06,2]&/@Transpose[{Sides[t],PedalLines[t,p]}]
},
{Blue,Line[{Coordinates[p],#}]&/@Vertices[t]
},
PointLabels[Join[
Transpose[{Point/@Vertices[t],{"A","B","C"}}],
Append[#,Red]&/@Transpose[{PedalPoints[t,p],{"(Subscript[P, A])","(Subscript[P, B])","(Subscript[P, C])"}}],
{{p,"P",Blue}}
],
{PointSize[.025],LabelOffset->-.04}
]
}],
PlotRange->All,
AspectRatio->Automatic]

Proof

pedal=FullSimplify[ExactTrilinears[{a,b,c}]]

eq=Simplify[Plus@@(Distance[pedal,#]&/@Permutations[{0,0,1}])-2Plus@@pedal,TriangleQ[{a,b,c}]]

Experimental`Resolve[
ForAll[{b,c},
TriangleQ[{a,b,c}],
eq≥0
]/.a->1]//Timing

Experimental`Resolve[
Exists[{b,c},
TriangleQ[{a,b,c}],
eq==0
]/.a->1]//Timing

Timing[soln=Reduce[eq==0&&TriangleQ[{a,b,c}]/.a->1,ReplaceValues->True]]

Oppenheim

TriangleQ[{a,b,c}]

Times@@(Distance[pedal,#]&/@Permutations[{0,0,1}])-Times@@Plus@@@Partition[pedal,2,1,1]

Timing[eq2=Simplify[Times@@(Distance[pedal,#]&/@Permutations[{0,0,1}])-Times@@Plus@@@Partition[pedal,2,1,1],TriangleQ[{a,b,c}]]]

Timing[eq2=FullSimplify[Times@@(Distance[pedal,#]&/@Permutations[{0,0,1}])-Times@@Plus@@@Partition[pedal,2,1,1],TriangleQ[{a,b,c}]]]

e1=((((a+b) (((a-b-c))^3) (((a+b-c))^3) (a+c) (((a-b+c))^3) (b+c) (((a+b+c))^3))/((((a^2)+(b^2)+(c^2)))^3))+8 √((1/((((a^2)+(b^2)+(c^2)))^6))((a^4) (b^4) (c^4) (2 (a^2)+2 (b^2)-(c^2)) (2 (a^2)-(b^2)+2 (c^2)) ((a^2)-2 ((b^2)+(c^2))) ((((a^4)+((((b^2)-(c^2)))^2)-2 (a^2) ((b^2)+(c^2))))^3))))/(8 ((((a+b-c) (a-b+c) (-a+b+c) (a+b+c)))^(3/2)));

e2=Simplify[((((a+b) (((a-b-c))^3) (((a+b-c))^3) (a+c) (((a-b+c))^3) (b+c) (((a+b+c))^3))/((((a^2)+(b^2)+(c^2)))^3))+((8(a^2) (b^2) (c^2))/((((a^2)+(b^2)+(c^2)))^3)) √(( (2 (a^2)+2 (b^2)-(c^2)) (2 (a^2)-(b^2)+2 (c^2)) ((a^2)-2 ((b^2)+(c^2))) ((((a^4)+((((b^2)-(c^2)))^2)-2 (a^2) ((b^2)+(c^2))))^3))))/(8 ((((a+b-c) (a-b+c) (-a+b+c) (a+b+c)))^(3/2)))]

LeafCount/@{e1,e2}

FullSimplify[(2 (a^2)+2 (b^2)-(c^2)) (2 (a^2)-(b^2)+2 (c^2)) ((a^2)-2 ((b^2)+(c^2))) ((((a^4)+((((b^2)-(c^2)))^2)-2 (a^2) ((b^2)+(c^2))))^3),TriangleQ[{a,b,c}]]

Experimental`Resolve[
ForAll[{b,c},
TriangleQ[{a,b,c}],
eq2≥0
]/.a->1]//Timing