Book I · Proposition 42

I.42

To construct, in a given rectilineal angle, a parallelogram equal to a given triangle.Heath, 1908

Every step, checked

• ABC is a genuine trianglegiven
• PQR is a genuine anglegiven
• the angle FEC equals the given angleby I.23
• FECG is a parallelogramby I.31
• the parallelogram is double the triangle AECby I.41
• and the triangle AEC is half of ABC, so the areas are equalby I.38

What it needs, and what needs it

Needs: I.10 I.23 I.31 I.38 I.41

Used by: I.44 I.45

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

Depth: 14 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 (×8)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×8)continuity

The proposition as code

@proposition(
    "I.42",
    CONSTRUCTION,
    sample=_triangle_and_angle,
)
def prop_I_42(a: Point, b: Point, c: Point, p: Point, q: Point, r: Point) -> Out:
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    hypothesis("PQR is a genuine angle", not collinear(p, q, r), guard=True)
    outline(p, q, r, close=False)  # the arms of the given angle

    middle = posit(prop_I_10(b, c).midpoint, "E")
    line(a, middle, "join AE")
    copied = prop_I_23(p, q, r, middle, c, beside=a)
    ray_point = posit(copied.ray_through, "S")

    through_a = _parallel_through(a, middle, c)
    f = posit(meet_one(through_a, line(middle, ray_point, "EF")), "F")
    through_c = _parallel_through(c, middle, f)
    g = posit(meet_one(through_c, through_a), "G")

    # FECG stands on the base EC with A on the parallel through F and G, which
    # is I.41's configuration. The other half of the argument is I.38 on the
    # triangles ABE and AEC: E bisects BC, so the bases are equal and lie on one
    # line, and both stand on A.
    because(prop_I_41, middle, c, g, f, a)
    because(prop_I_38, b, middle, a, middle, c, a)

    claim("the angle FEC equals the given angle", "I.23", eq_angle(f, middle, c, p, q, r))
    claim("FECG is a parallelogram",
          "I.31",
          parallel(Line.through(f, middle), Line.through(g, c))
          and parallel(Line.through(f, g), Line.through(middle, c)))
    claim("the parallelogram is double the triangle AEC", "I.41",
          _area(f, middle, c, g) == 2 * _area(a, middle, c))
    claim("and the triangle AEC is half of ABC, so the areas are equal", "I.38",
          _area(f, middle, c, g) == _area(a, b, c))
    return Out(parallelogram=(f, middle, c, g), angle_at=middle)