Book V · Proposition 19

V.19

If, as a whole is to a whole, so is a part subtracted to a part subtracted, the remainder will also be to the remainder as whole to whole.Heath, 1908

Every step, checked

• the magnitudes are positivegiven
• whole is to whole as part is to partgiven
• the parts are less than the wholesgiven
• the remainder is to the remainder as whole to wholeby Def.5

What it needs, and what needs it

Needs: nothing earlier.

Used by: V.25

Rests on: Def.5

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.19",
    THEOREM,
    sample=_a_proper_part_in_proportion,
)
def prop_V_19(a, b, c, d) -> Out:
    """The whole AB is to the whole CD as the part AE to the part CF."""
    hypothesis("the magnitudes are positive",
               all(sign(x) > 0 for x in (a, b, c, d)), guard=True)
    hypothesis("whole is to whole as part is to part", a * d == b * c)
    hypothesis("the parts are less than the wholes",
               sign(a - c) > 0 and sign(b - d) > 0)
    claim("the remainder is to the remainder as whole to whole", "Def.5",
          separating_witness(a - c, b - d, a, b) is None)
    return Out(remainders=(a - c, b - d))