Book X · Proposition 42

X.42

A binomial straight line is divided into its terms at one point only.Heath, 1908

Every step, checked

What it needs, and what needs it

Needs: nothing earlier.

Used by: X.43 X.44 X.45 X.46 X.47

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(ref, THEOREM, sample=_kind_sample(kind))
def _divided(a, b, _kind=kind) -> Out:
    whole = a + b
    named = classify(whole)
    # X.42 divides a binomial; X.43 to X.47 are the same argument for
    # the other five compounds, so each hands it its own kind.
    if ref != "X.42":
        because(get("X.42").wrapped, a, b, _kind)
    hypothesis(f"the whole is a {ADDED_NAMES[_kind]}",
               named.name == ADDED_NAMES[_kind] or named.family == ADDED_NAMES[_kind])
    claim("the division into terms is recovered from the line itself",
          "X.42", len(named.terms) == 2)
    claim("and those two terms add back to it, so the point of division "
          "is the only one", "X.42",
          is_zero(named.terms[0] + named.terms[1] - whole))
    return Out(terms=tuple(named.terms))