G.145 converse of the tangent-secant theorem

III.37

If from a point outside a circle a secant and a segment to the circle are drawn such that the rectangle on the whole secant and its external part equals the square on the segment, the segment is tangent to the circle.

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

given D outside ( A B C ), secant / D C A /, / D B / with rect(/ A D /, / C D /) = :g:`/ D B / <g1:/ D B />`²

prove / D B / touches ( A B C ) at B

∵ circle_radiigiven rect(/ A D /, / C D /) = :g:`/ D B / <g1:/ D B />`²

∵ tangent_to_circle, find_circle_center, segmentconstruct tangent_to_circle(D, ( A B C )) → tangent / D E /, find_circle_center(( A B C )) → F, segment(F, E, B, D) → / F E /, / F B /, / F D /

∵ radius_perpendicular_to_tangent, tangent_secant_theorem, equal_transitiveassert < F E D ) is right and rect(/ A D /, / C D /) = DEg/ D B / <g1:/ D B />` = / D E /

∵ circle_radii, sss_congruenceassert / F B / = / F E /, / F D / common, / D B / = / D E / → < D B F ) = < F E D ) is right

∵ perpendicular_at_diameter_extremity_tangent∴ / D B / ⊥ / F B / at extremity B → / D B / touches ( A B C )

Dependency Graph

Required for

G.162, G.163, G.164