Problem (2007CTSTp2): Let $ I$ be the incenter of triangle $ ABC.$ Let $ M,N$ be the midpoints of $ AB,AC,$ respectively. Points $ D,E$ lie on $ AB,AC$ respectively such that $ BD=CE=BC.$ The line perpendicular to $ IM$ through $ D$ intersects the line perpendicular to $ IN$ through $ E$ at $ P.$ Prove that
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; m = midpoint a b; n = midpoint a c; d = on_line a b, on_circle b c; e = on_line a c, on_circle c b; p = on_tline d i m, on_tline e i n ? perp a p b c
HAGeo formalization: A B C = triangle; I = incenter A B C; M = midpoint A B; N = midpoint A C; AB = line A B; (B,C) = circle_center_point B C; D = intersection AB (B,C); AC = line A C; (C,B) = circle_center_point C B; E = intersection AC (C,B); IM = line I M; l1 = perpendicular_line D IM; IN = line I N; l2 = perpendicular_line E IN; P = intersection l1 l2; AP = line A P; BC = line B C; Prove: perpendicular AP BC
Difficulty score: 3.6