G.142 cut off a circle segment admitting a given angle

III.34

From a given circle, cut off a segment admitting an angle equal to a given rectilineal angle.

cut_circle_segment_with_angle(( A B C ), < D )) → ( B A C )

given ( A B C ), < D )

construct < B A C ) in segment ( B A C ) cut off from ( A B C ) = < D )

∵ circle_radii, rectilineal_angle_defgiven circle ( A B C ), rectilineal angle < D )

∵ perpendicular_at_diameter_extremity_tangentconstruct tangent / E F / touching ( A B C ) at B

∵ copy_angleconstruct copy_angle(/ F B /, B, < D )) → < F B C ) = < D ) with chord / B C /

∵ alternate_segment_theoremassert tangent / E F / and chord / B C / at B → < F B C ) = < B A C ) in alternate segment ( B A C )

∵ equal_transitive, angle_segment_angle_def∴ < F B C ) = < D ) → < B A C ) = < D ) in segment ( B A C )

Dependency Graph