Book VII · Proposition 35

VII.35

If two numbers measure any number, the least number measured by them will also measure the same.Heath, 1908

Every step, checked

• both are numbersgiven
• both measure the common multipleby Def.VII.3
• so the least they measure also measures itby VII.35

What it needs, and what needs it

Needs: nothing earlier.

Used by: VII.36

Rests on: Def.VII.3

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.35",
    THEOREM,
    sample=lambda rng: (rng.randint(2, 30), rng.randint(2, 30), rng.randint(2, 10)),
)
def prop_VII_35(a: int, b: int, times: int) -> Out:
    hypothesis("both are numbers", a > 1 and b > 1 and times > 0, guard=True)
    common = lcm(a, b) * times
    claim("both measure the common multiple", "Def.VII.3",
          measures(a, common) and measures(b, common))
    claim("so the least they measure also measures it", "VII.35",
          measures(lcm(a, b), common))
    return Out(least=lcm(a, b))