Book V · Proposition 17

V.17

If magnitudes be proportional componendo, they will also be proportional separando.Heath, 1908

Separando. Euclid needs both this and its converse because a ratio is not a quotient he may rearrange at will.

Every step, checked

• the magnitudes are positivegiven
• componendo: (a+b) : b = (c+d) : dgiven
• separando, a : b = c : dby 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.17",
    THEOREM,
    sample=_proportional_magnitudes,
    note="Separando. Euclid needs both this and its converse because a ratio is "
    "not a quotient he may rearrange at will.",
)
def prop_V_17(a, b, c, d) -> Out:
    """AB : BE = CD : DF, componendo; separando follows."""
    hypothesis("the magnitudes are positive",
               all(sign(x) > 0 for x in (a, b, c, d)), guard=True)
    hypothesis("componendo: (a+b) : b = (c+d) : d", (a + b) * d == b * (c + d))
    claim("separando, a : b = c : d", "Def.5",
          separating_witness(a, b, c, d) is None)
    return Out()