Book VII · Proposition 15

VII.15

If an unit measure any number, and another number measure any other number the same number of times, alternately also, the unit will measure the third number the same number of times that the second measures the fourth.Heath, 1908

Every step, checked

• the numbers are genuinegiven
• the multiplier measures the product as often as the unit measures the numbergiven
• the unit measures the number as many times as the number has unitsby Def.VII.2
• and alternately, the unit is to the multiplier as the number is to the productby VII.15

What it needs, and what needs it

Needs: nothing earlier.

Rests on: Def.VII.2

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.15",
    THEOREM,
    sample=lambda rng: _measured_the_same_number_of_times(rng),
)
def prop_VII_15(number: int, times: int, product: int) -> Out:
    """A unit measures a number as that number measures its multiple."""
    hypothesis("the numbers are genuine", number > 1 and times > 1, guard=True)
    # The product is given rather than built. Built, both claims below compared
    # it with the expression it had just been assigned.
    hypothesis("the multiplier measures the product as often as the unit "
               "measures the number",
               measures(times, product) and product // times == number)
    claim("the unit measures the number as many times as the number has units",
          "Def.VII.2", measures(1, number) and product // times == number)
    claim("and alternately, the unit is to the multiplier as the number is to "
          "the product", "VII.15",
          measures(number, product) and product // number == times)
    return Out(product=product)