Book VII · Proposition 39

VII.39

To find the number which is the least that will have given parts.Heath, 1908

The least number having given parts is the least common multiple of their names -- the last proposition of Book VII, and the one Book IX uses.

Every step, checked

What it needs, and what needs it

Needs: VII.36 VII.38

Rests on: Def.VII.3

Depth: 2 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(
    "VII.39",
    CONSTRUCTION,
    sample=lambda rng: (rng.randint(2, 12), rng.randint(2, 12), rng.randint(2, 12)),
    note="The least number having given parts is the least common multiple of "
    "their names -- the last proposition of Book VII, and the one Book IX uses.",
)
def prop_VII_39(a: int, b: int, c: int) -> Out:
    hypothesis("the parts are genuine", a > 1 and b > 1 and c > 1, guard=True)
    least = lcm(lcm(a, b), c)
    because(prop_VII_36, a, b, c)
    because(prop_VII_38, a, lcm(a, b)) if measures(a, lcm(a, b)) and a > 1 else None

    claim("the number found has all three parts", "VII.38",
          all(measures(n, least) for n in (a, b, c)))
    claim("and no smaller number has them all", "VII.36",
          not any(all(measures(n, m) for n in (a, b, c)) for m in range(1, least)))
    return Out(least=least)