G.106 distances to a circle from an exterior point

III.8

From a point outside a circle, of segments falling on the concave arc the greatest passes through the center and nearer ones are greater, while on the convex arc the least lies between the point and the diameter and nearer ones are less, with at most two equal segments.

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

given ( A B C ), exterior point D, secants / D A / (through center), / D E /, / D F /, / D C /

prove / D A / > / D E / > / D F / > / D C /, / D G / < / D K / < / D L / < / D H /, and / D K / = / D B / (unique pair)

∵ circle_radii, circle_diametergiven ( A B C ), exterior point D, secants / D A / (cutting at G), / D E / (K), / D F / (L), / D C / (H)

∵ find_circle_center, segment, copy_angleconstruct find_circle_center(( A B C )) → M; join radii / M E /, / M F /, / M C /, / M K /, / M L /, / M H /; copy_angle(/ M D /, M, < K M D )) → < D M B ) = < K M D ), join / D B /

∵ triangle_inequality, hinge_theoremassert / D A / = / M E / + / M D / > / D E /; < E M D ) > < F M D ) → / D E / > / D F / > / D C /

∵ triangle_inequality, interior_triangle_boundsassert / M K / + / D K / > / M D / and / M G / = / M K / → / D G / < / D K /; / M K / + / D K / < / M L / + / D L / → / D K / < / D L / < / D H /

∵ sas_congruence, equal_transitiveassert < M K D > ≃ < M B D > → / D K / = / D B /; if / D N / = / D K / then / D B / = / D N / ⇒⇐

∴ / D A / > / D E / > / D F / > / D C /, / D G / < / D K / < / D L / < / D H /, and only two equal segments / D K / = / D B / fall from D

Dependency Graph