Book VII · Proposition 7

VII.7

If a number be that part of a number, which a number subtracted is of a number subtracted, the remainder will also be the same part of the remainder that the whole is of the whole.Heath, 1908

Every step, checked

• the subtraction is a proper onegiven
• each is the same part of its ownby Def.VII.3
• so the remainder is the same part of the remainderby VII.7

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.7",
    THEOREM,
    sample=lambda rng: (rng.randint(2, 12), rng.randint(4, 30), rng.randint(1, 3)),
)
def prop_VII_7(times: int, whole: int, taken: int) -> Out:
    """A part subtracted from a part leaves the same part of the remainder."""
    hypothesis("the subtraction is a proper one", whole > taken > 0 and times > 1, guard=True)
    big, small = whole * times, taken * times
    claim("each is the same part of its own", "Def.VII.3",
          big == whole * times and small == taken * times)
    claim("so the remainder is the same part of the remainder", "VII.7",
          big - small == (whole - taken) * times)
    return Out(remainder=whole - taken)