Book V · Proposition 6

V.6

If two magnitudes be equimultiples of two magnitudes, and any magnitudes subtracted from them be equimultiples of the same, the remainders also are either equal to the same or equimultiples of them.Heath, 1908

Every step, checked

• the magnitudes are positivegiven
• less is taken away than there isgiven
• the remainders are equimultiples of the same two magnitudesby V.1
• and where one multiple remains they are equal to themby C.N.3

What it needs, and what needs it

Needs: V.1

Rests on: C.N.2, C.N.3, Def.2

Depth: 1 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.6",
    THEOREM,
    sample=_two_magnitudes_and_two_multiples,
)
def prop_V_6(x, y, times: int, taken: int) -> Out:
    """AB and CD are `times` E and F; `taken`-fold E and F are subtracted."""
    hypothesis("the magnitudes are positive", sign(x) > 0 and sign(y) > 0, guard=True)
    hypothesis("less is taken away than there is", taken <= times)
    left, right = times * x - taken * x, times * y - taken * y
    remaining = times - taken
    if remaining >= 1:
        because(prop_V_1, x, y, remaining)

    claim("the remainders are equimultiples of the same two magnitudes", "V.1",
          left == remaining * x and right == remaining * y)
    claim("and where one multiple remains they are equal to them", "C.N.3",
          remaining != 1 or (left == x and right == y))
    return Out(remainders=(left, right))