Book VII · Proposition 14

VII.14

If there be as many numbers as we please, and others equal to them in multitude, which taken two and two are in the same ratio, they will also be in the same ratio ex aequali.Heath, 1908

Every step, checked

What it needs, and what needs it

Needs: VII.13

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(
    "VII.14",
    THEOREM,
    sample=lambda rng: (rng.randint(2, 20), rng.randint(2, 20), rng.randint(2, 20),
                        rng.randint(2, 8)),
)
def prop_VII_14(a: int, b: int, c: int, scale: int) -> Out:
    """Three numbers and three more, in the same ratio two and two."""
    hypothesis("the numbers are genuine", a > 1 and b > 1 and c > 1 and scale > 1, guard=True)
    d, e, f = a * scale, b * scale, c * scale
    # A : B as D : E, so VII.13 takes them alternately. Written as a conditional
    # appeal on (a, b, c, scale * c), whose condition asks a * scale == b, this
    # never once ran -- and was written twice.
    because(prop_VII_13, a, b, d, e)
    because(prop_VII_13, b, c, e, f)

    claim("the pairs are in the same ratio", "VII.13", a * e == b * d and b * f == c * e)
    claim("so ex aequali the first is to the third as the fourth to the sixth",
          "VII.14", a * f == c * d)
    return Out()