Book VIII · Proposition 16

VIII.16

If a square number do not measure a square number, neither will the side measure the side; and, if the side do not measure the side, neither will the square measure the square.Heath, 1908

Every step, checked

• the sides are genuine numbersgiven
• if the square does not measure the square, neither does the sideby VIII.14

What it needs, and what needs it

Needs: VIII.14

Depth: 1 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(
    "VIII.16",
    THEOREM,
    sample=lambda rng: (rng.randint(2, 15), rng.randint(2, 15)),
)
def prop_VIII_16(a: int, b: int) -> Out:
    """The contrapositive of VIII.14, which Euclid states separately."""
    hypothesis("the sides are genuine numbers", a > 1 and b > 1, guard=True)
    because(prop_VIII_14, a, b)

    claim("if the square does not measure the square, neither does the side",
          "VIII.14", (not measures(a * a, b * b)) == (not measures(a, b)))
    return Out()