Book VII · Proposition 16

VII.16

If two numbers by multiplying one another make certain numbers, the numbers so produced will be equal to one another.Heath, 1908

Multiplication commutes. Euclid has to prove it, because his product is 'a taken b times' and that is not obviously the same as b taken a times.

Every step, checked

• both are numbersgiven
• a taken b times equals b taken a timesby VII.16

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.16",
    THEOREM,
    sample=lambda rng: (rng.randint(2, 60), rng.randint(2, 60)),
    note="Multiplication commutes. Euclid has to prove it, because his product "
    "is 'a taken b times' and that is not obviously the same as b taken a times.",
)
def prop_VII_16(a: int, b: int) -> Out:
    hypothesis("both are numbers", a > 1 and b > 1, guard=True)
    claim("a taken b times equals b taken a times", "VII.16",
          _taken(a, b) == _taken(b, a))
    return Out(product=_taken(a, b))