G.107 point with three equal segments to a circle is the center

III.9

A point within a circle from which more than two equal segments fall on the circle is the center of the circle.

three_equal_radii_center(( A B C ), D, / D A /, / D B /, / D C /)

given ( A B C ), interior point D, / D A / = / D B / = / D C /

prove D = center(( A B C ))

∵ circle_radiigiven ( A B C ), interior point D, / D A / = / D B / = / D C /

∵ segment, bisect_segment, extendconstruct join / A B /, / B C /, bisect at E, F (/ A E / = / E B /, / B F / = / F C /), draw / G K / through E, D and / H L / through F, D

∵ sss_congruence, right_angle_perpendicularassert < A E D > ≃ < B E D > → < A E D ) = < B E D ) (right) → / G K / ⊥ / A B /

∵ find_circle_centerassert / G K / bisects / A B / ⊥ → center(( A B C )) ∈ / G K /; similarly center(( A B C )) ∈ / H L /

∵ circle_center∴ / G K / ∩ / H L / = D → D = center(( A B C ))

Dependency Graph

Required for

G.130