Book VII · Proposition 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.
Rests on: Def.VII.3
Depth: 2 steps of argument above the first principles. Parallel postulate: not needed.
Nothing. It draws no intersections and reads nothing off the picture.
@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)