Book VII · Proposition 6

VII.6

If a number be parts of a number, and another be the same parts of another, the sum will also be the same parts of the sum that the one is of the one.Heath, 1908

Every step, checked

• the fraction is a genuine onegiven
• it applies to both numbers exactlygiven
• each is the same parts of its ownby Def.VII.4
• so the sum is the same parts of the sumby VII.6

What it needs, and what needs it

Needs: nothing earlier.

Rests on: Def.VII.4

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.6",
    THEOREM,
    sample=_same_parts_of_two,
)
def prop_VII_6(numerator: int, denominator: int, first: int, second: int) -> Out:
    """The 'parts' version of VII.5: a fraction, not just a unit fraction."""
    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("each is the same parts of its own", "Def.VII.4",
          a * denominator == first * numerator and b * denominator == second * numerator)
    claim("so the sum is the same parts of the sum", "VII.6",
          (a + b) * denominator == (first + second) * numerator)
    return Out(sum=a + b)