Book IV · Proposition 10

IV.10

To construct an isosceles triangle having each of the angles at the base double of the remaining one.Heath, 1908

The triangle that makes the pentagon possible: its base angles are double the apex, which puts 36 degrees within reach of the compass.

Every step, checked

• A and B are distinctgiven
• BD equals the greater segment ACby I.3
• the triangle is isosceles, AB and AD both radiiby Def.15
• each angle at the base is double the angle at the apexby II.11, III.32

What it needs, and what needs it

Needs: I.3 II.11 III.32

Rests on: C.N.1, C.N.2, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.22, Def.3, Def.4, Post.1, Post.5

Depth: 16 steps of argument above the first principles. Parallel postulate: needed.

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×23)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×46)continuity

The proposition as code

@proposition(
    "IV.10",
    CONSTRUCTION,
    sample=samples.segment,
    note="The triangle that makes the pentagon possible: its base angles are "
    "double the apex, which puts 36 degrees within reach of the compass.",
)
def prop_IV_10(a: Point, b: Point) -> Out:
    """Cut AB in extreme and mean ratio, and step the greater segment off the
    circle about A."""
    hypothesis("A and B are distinct", a != b)
    section = prop_II_11(a, b).section
    around = circle(a, b, "circle centre A through B")
    reach = circle_with_radius2(b, len2(a, section), "circle centre B with radius AC")
    d = posit(meet(reach, around)[0], "D")
    outline(a, b, d)
    line(section, d, "CD")

    because(prop_I_3, a, b, section, a)
    # The base angle is read off the circle about the triangle BCD, where BD
    # touches it: III.32 is the step that makes it equal to the angle at A.
    _about = _centre_of(b, section, d)
    if not collinear(b, section, d):
        because(prop_III_32, _about, b, section, d)

    claim("BD equals the greater segment AC", "I.3", eq_len(b, d, a, section))
    claim("the triangle is isosceles, AB and AD both radii", "Def.15", eq_len(a, b, a, d))
    claim("each angle at the base is double the angle at the apex", ["II.11", "III.32"],
          angle_at(a, b, d) == angle_at(b, a, d).doubled()
          and angle_at(a, d, b) == angle_at(b, a, d).doubled())
    return Out(triangle=(a, b, d), section=section)