Book V · Proposition 5

V.5

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

Every step, checked

• the magnitudes are positivegiven
• the part subtracted is less than the wholegiven
• the remainder is the same multiple of the remainderby C.N.3

What it needs, and what needs it

Needs: nothing earlier.

Rests on: C.N.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(
    "V.5",
    THEOREM,
    sample=_a_part_of_a_whole,
)
def prop_V_5(whole, part, times: int) -> Out:
    """AB is `times` CD, and the part taken away is the same multiple of a part."""
    hypothesis("the magnitudes are positive", sign(whole) > 0 and sign(part) > 0, guard=True)
    hypothesis("the part subtracted is less than the whole", sign(whole - part) > 0)
    ab, cd = times * whole, times * part
    claim("the remainder is the same multiple of the remainder", "C.N.3",
          ab - cd == times * (whole - part))
    return Out(remainder=ab - cd)