Book VII · Proposition 34

VII.34

Given two numbers, to find the least number which they measure.Heath, 1908

Every step, checked

• both are numbersgiven
• the number found is measured by bothby VII.34
• and nothing less isby VII.34

What it needs, and what needs it

Needs: nothing earlier.

Used by: VII.36 VIII.4

Depth: 0 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.34",
    CONSTRUCTION,
    sample=lambda rng: (rng.randint(2, 60), rng.randint(2, 60)),
)
def prop_VII_34(a: int, b: int) -> Out:
    hypothesis("both are numbers", a > 1 and b > 1, guard=True)
    least = lcm(a, b)
    claim("the number found is measured by both", "VII.34",
          measures(a, least) and measures(b, least))
    claim("and nothing less is", "VII.34",
          not any(measures(a, n) and measures(b, n) for n in range(1, least)))
    return Out(least=least)