Book V · Proposition 16

V.16

If four magnitudes be proportional, they will also be proportional alternately.Heath, 1908

Every step, checked

• a : b = c : dgiven
• the magnitudes are of the same kind and nonzerogiven
• alternately, a : c = b : d -- no equimultiples separate the alternated ratios eitherby 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.16",
    THEOREM,
    sample=_proportional_magnitudes,
)
def prop_V_16(a, b, c, d) -> Out:
    hypothesis("a : b = c : d", a * d == b * c)
    hypothesis("the magnitudes are of the same kind and nonzero",
               not is_zero(a) and not is_zero(b) and not is_zero(c) and not is_zero(d), guard=True)
    claim("alternately, a : c = b : d -- no equimultiples separate the alternated "
          "ratios either", "Def.5", separating_witness(a, c, b, d) is None)
    return Out()