Book VII · Proposition 5

VII.5

If a number be a part of a number, and another be the same part of another, the sum will also be the same part of the sum that the one is of the one.Heath, 1908

Every step, checked

• the first is a part of the secondgiven
• the third is the same part of the fourthgiven
• the two stand in the same partby Def.VII.3
• so the sum is the same part of the sumby VII.5

What it needs, and what needs it

Needs: nothing earlier.

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.5",
    THEOREM,
    sample=_same_part_of_two,
)
def prop_VII_5(part: int, whole: int, other: int, other_whole: int) -> Out:
    """`part` is a part of `whole`; `other` is the same part of its own whole."""
    hypothesis("the first is a part of the second", measures(part, whole) and part > 0)
    # The fourth number is a given and not built from the third. Building it as
    # ``other * times`` made the claim below compare it with what it had just
    # been assigned, which no configuration could refute.
    hypothesis("the third is the same part of the fourth",
               measures(other, other_whole) and other > 0
               and other_whole // other == whole // part)
    times = whole // part
    claim("the two stand in the same part", "Def.VII.3",
          whole == part * times and other_whole == other * times)
    claim("so the sum is the same part of the sum", "VII.5",
          whole + other_whole == (part + other) * times)
    return Out(sum=part + other)