Book VII · Proposition 9

VII.9

If a number be a part of a number, and another be the same part of another, alternately also, whatever part or parts the first is of the third, the same part, or the same parts, will the second also be of the fourth.Heath, 1908

Every step, checked

• the first is a part of the secondgiven
• the third is the same part of the fourthgiven
• alternately, the first is to the third as the second to the fourthby VII.9

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.9",
    THEOREM,
    sample=_same_part_of_two,
)
def prop_VII_9(part: int, whole: int, other: int, other_whole: int) -> Out:
    """Alternation for parts: if A is a part of B as C is of D, then A:C = B:D."""
    hypothesis("the first is a part of the second", measures(part, whole) and part > 0)
    hypothesis("the third is the same part of the fourth",
               measures(other, other_whole) and other > 0
               and other_whole // other == whole // part)
    claim("alternately, the first is to the third as the second to the fourth",
          "VII.9", part * other_whole == whole * other)
    return Out()