← elements / Elements 2.0 (G Index)

G.255 number part parts¶

Any number is either a part or parts of any number, the less of the greater.

number_part_parts(A, / B C /)
given A, / B C / be two numbers, let / B C / be the less
prove / B C / is either a part, or parts, of A

given A, / B C / be two numbers, let / B C / be the less

assert For A, / B C / are either prime to one another or not

assert First, let A, / B C / be prime to one another

assert If / B C / be divided into the units in it, each unit of those in / B C / will be some part of A

assert So that / B C / is parts of A

assert Next let A, / B C / not be prime to one another

assert Then / B C / either measures, or does not measure, A

assert If now / B C / measures A, / B C / is a part of A

construct numbers_prime_find: But, if not, let the greatest common measure D of A, / B C / be taken

assert let / B C / be divided into the numbers = to D, namely / B E /, / E F /, / F C /

assert D measures A, D is a part of A

assert D = each of the numbers / B E /, / E F /, / F C /

assert each of the numbers / B E /, / E F /, / F C / is also a part of A

∴ So that / B C / is parts of A

Dependency Graph¶