Book V · Proposition 1

V.1

If there be any number of magnitudes whatever which are, respectively, equimultiples of any magnitudes equal in multitude, then, whatever multiple one of the magnitudes is of one, that multiple also will all be of all.Heath, 1908

Multiplication distributes over addition, said of magnitudes that are not numbers and cannot be multiplied by one another.

Every step, checked

What it needs, and what needs it

Needs: nothing earlier.

Used by: V.2 V.3 V.6

Rests on: C.N.2, Def.2

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.1",
    THEOREM,
    sample=_two_magnitudes_and_a_multiple,
    note="Multiplication distributes over addition, said of magnitudes that are "
    "not numbers and cannot be multiplied by one another.",
)
def prop_V_1(e, f, times: int) -> Out:
    """AB and CD are the same multiple of E and F."""
    hypothesis("the magnitudes are positive", sign(e) > 0 and sign(f) > 0, guard=True)
    hypothesis("the multiple is a genuine one", times >= 1, guard=True)
    ab, cd = times * e, times * f
    claim("AB is that multiple of E, and CD of F", "Def.2",
          ab == times * e and cd == times * f)
    claim("so their sum is the same multiple of the sum", "C.N.2",
          ab + cd == times * (e + f))
    return Out(sum=ab + cd)