Book IX · Proposition 1

IX.1

If two similar plane numbers by multiplying one another make some number, the product will be square.Heath, 1908

Every step, checked

• the sides are genuine numbersgiven
• the two are similar plane numbers, their sides proportionalgiven
• their product is squareby IX.1

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(
    "IX.1",
    THEOREM,
    sample=similar_planes,
)
def prop_IX_1(a: int, b: int, c: int, d: int) -> Out:
    hypothesis("the sides are genuine numbers",
               a > 1 and b > 1 and c > 1 and d > 1, guard=True)
    hypothesis("the two are similar plane numbers, their sides proportional",
               a * d == b * c)
    first, second = a * b, c * d
    claim("their product is square", "IX.1", is_square(first * second))
    return Out(product=first * second)