Book VII · Proposition 10

VII.10

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

Every step, checked

• the fraction is a genuine onegiven
• it applies to both numbers exactlygiven
• alternately, the first is to the third as the second to the fourthby VII.10

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.10",
    THEOREM,
    sample=_same_parts_of_two,
)
def prop_VII_10(numerator: int, denominator: int, first: int, second: int) -> Out:
    """The 'parts' version of VII.9."""
    hypothesis("the fraction is a genuine one", denominator > numerator > 0, guard=True)
    hypothesis("it applies to both numbers exactly",
               measures(denominator, first) and measures(denominator, second))
    a = first * numerator // denominator
    b = second * numerator // denominator
    claim("alternately, the first is to the third as the second to the fourth",
          "VII.10", a * second == first * b)
    return Out()