G.163 inscribe a regular pentagon in a circle

IV.11

Inscribe an equilateral and equiangular pentagon in a given circle.

inscribe_pentagon_in_circle(( A B C D E )) → < A B C D E >

given ( A B C D E ) is a given circle

construct < A B C D E > is an equilateral and equiangular pentagon inscribed in ( A B C D E )

∵ circle_radii, polygon_said_inscribed_defgiven ( A B C D E ) is the given circle

∵ golden_isosceles_triangle, inscribe_triangle_in_circleconstruct golden_isosceles_triangle() → < F G H > (< F G H ) = < F H G ) = 2 < G F H )), inscribe_triangle_in_circle(( A B C D E ), < F G H >) → < A C D > (< A C D ) = < C D A ) = 2 < C A D ))

∵ bisect_angle, segmentconstruct bisect_angle(< A C D )) → / C E /, bisect_angle(< C D A )) → / D B /, segment(A, B, C, D, E) → / A B /, / B C /, / D E /, / E A /

∵ equal_angles_equal_arcs, equal_arcs_equal_chordsassert < C A D ) = < A C E ) = < E C D ) = < C D B ) = < B D A ) → arcs ( A B ) = ( B C ) = ( C D ) = ( D E ) = ( E A ) → sides / A B / = / B C / = / C D / = / D E / = / E A /

∵ add_equals, equal_arcs_equal_anglesassert ( A B ) = ( D E ) + ( B C D ) → ( A B C D ) = ( E D C B ) → < A E D ) = < B A E ) = < A B C ) = < B C D ) = < C D E )

∵ polygon_said_inscribed_def∴ < A B C D E > is an equilateral and equiangular pentagon inscribed in ( A B C D E )

Dependency Graph

Required for

G.164