Book IX · Proposition 19

IX.19

Given three numbers, to investigate when it is possible to find a fourth proportional to them.Heath, 1908

Every step, checked

• all three are numbersgiven
• a fourth proportional exists exactly when the first measures the product of the second and thirdby VII.19
• and when it does, it is that quotientby VII.19

What it needs, and what needs it

Needs: VII.19

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

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(
    "IX.19",
    CONSTRUCTION,
    sample=_fourth_proportional_case,
)
def prop_IX_19(a: int, b: int, c: int) -> Out:
    hypothesis("all three are numbers", a > 1 and b > 1 and c > 1, guard=True)
    possible = measures(a, b * c)
    if possible and b * c // a > 1:
        because(prop_VII_19, a, b, c, b * c // a)

    claim("a fourth proportional exists exactly when the first measures the "
          "product of the second and third", "VII.19", possible == (b * c % a == 0))
    claim("and when it does, it is that quotient", "VII.19",
          not possible or a * (b * c // a) == b * c)
    return Out(possible=possible, fourth=(b * c // a) if possible else None)