Book V · Proposition 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.
Needs: nothing earlier.
Rests on: C.N.2, Def.2
Depth: 0 steps of argument above the first principles. Parallel postulate: not needed.
Nothing. It draws no intersections and reads nothing off the picture.
@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)