G.373 less unequal magnitudes¶
If, when the less of two unequal magnitudes is continually subtracted in turn from the greater, that which is left never measures the one before it, the magnitudes is incommensurable.
less_unequal_magnitudes()
prove the magnitudes / A B /, / C D / are incommensurable
assert There being two unequal magnitudes / A B /, / C D /, and / A B / being the less, when the less is continually subtracted in turn from the greater, let that which is left over never measure the one before it
assert If they are commensurable, some magnitude will measure them
assert Let a magnitude measure them, if possible, and let it be E
assert Let / A B /, measuring / F D /, leave / C F / less than itself, let / C F / measuring / B G /, leave / A G / less than itself, and let this process be repeated continually, until there is left some magnitude which < E
assert Suppose this done, and let there be left / A G / less than E
assert E measures / A B /, while / A B / measures / D F /,
assert E will also measure / F D /
assert It measures / C D / also
assert it will also measure / C F /
assert / C F / measures / B G /
assert E also measures / B G /
assert It measures / A B / also
assert it will also measure / A G /, the greater the less :
assert ⇒⇐
∵ magnitudes_said_commensurable_def∴ no magnitude will measure the magnitudes / A B /, / C D /; therefore the magnitudes / A B /, / C D / are incommensurable