Formalized:
a b d = triangle a b d; c = on_circle c a b; m = midpoint m b c; e = on_line a d, eqangle3 b a b a d; o = circle o b d c; u = midpoint u a d; k = on_circle k o b, on_circle k u d; r = circle r a m k ? cyclic a k m e
Example proof:
- Let KD and BC intersect at T and construct L on AK such that $AK \times AL=AB^2$.
- Since <BEA=<ABD, so $AD \times AE=AB^2=AK \times AL$ so DKLE cyclic.
- So E, L is the inverse of D, K with origin A and radius AB (=AC).
- Since BDKC is cyclic by definition of K, BELC is cyclic by inversion (or you can prove this using plain angle chasing).
- So <DEL=<AKD=pi/2
- By the radical axis theorem on circles BDKC, BELC, DKEL gives TEL is collinear.
- So <TEA=pi/2
- Since <TMA=<TKA=pi/2 by definition of T and K, so AKME is cyclic on the circle of diameter AT.
Btw you can also prove this using purely length chasing, here not shown.
Formalized:
a b d = triangle a b d; c = on_circle c a b; m = midpoint m b c; e = on_line a d, eqangle3 b a b a d; o = circle o b d c; u = midpoint u a d; k = on_circle k o b, on_circle k u d; r = circle r a m k ? cyclic a k m eExample proof:
Btw you can also prove this using purely length chasing, here not shown.