Book V · Proposition 9

V.9

Magnitudes which have the same ratio to the same are equal to one another; and magnitudes to which the same has the same ratio are equal.Heath, 1908

Definition 5 executed in both directions: equal ratios admit no separating equimultiples, and unequal magnitudes always do.

Every step, checked

• a : b = c : dgiven
• no equimultiples up to the searched bound separate the ratiosby Def.5
• and none exist at allby Def.5
• so a magnitude having this ratio to b is determined uniquelyby Def.5

What it needs, and what needs it

Needs: nothing earlier.

Rests on: Def.5

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(
    "V.9",
    THEOREM,
    sample=_proportional_magnitudes,
    note="Definition 5 executed in both directions: equal ratios admit no separating "
    "equimultiples, and unequal magnitudes always do.",
)
def prop_V_9(a, b, c, d) -> Out:
    hypothesis("a : b = c : d", a * d == b * c)
    claim("no equimultiples up to the searched bound separate the ratios", "Def.5",
          eudoxus_same_ratio(a, b, c, d, bound=20))
    claim("and none exist at all", "Def.5", separating_witness(a, b, c, d) is None)
    claim("so a magnitude having this ratio to b is determined uniquely", "Def.5",
          separating_witness(a, b, a * 2, b * 2) is None)
    return Out()