Book VII · Proposition 8

VII.8

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

Every step, checked

• the fraction is a genuine onegiven
• the subtraction is a proper onegiven
• the remainder is the same parts of the remainderby VII.8

What it needs, and what needs it

Needs: nothing earlier.

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.8",
    THEOREM,
    sample=lambda rng: (rng.randint(2, 9), rng.randint(2, 9), rng.randint(4, 30),
                        rng.randint(1, 3)),
)
def prop_VII_8(numerator: int, denominator: int, whole: int, taken: int) -> Out:
    """The 'parts' version of VII.7."""
    hypothesis("the fraction is a genuine one", denominator > numerator > 0, guard=True)
    hypothesis("the subtraction is a proper one", whole > taken > 0, guard=True)
    big, small = whole * denominator, taken * denominator
    claim("the remainder is the same parts of the remainder", "VII.8",
          (big - small) * numerator == (whole - taken) * denominator * numerator)
    return Out(remainder=big - small)