G.260 number parts number

VII.8

If a number be the same parts of a number that a number subtracted is of a number subtracted, the remainder is the same parts of the remainder that the whole is of the whole.

number_parts_number_vii_8()

prove / E B / is also the same parts of / F D / that / A B / is of / C D /

assert Let the number / A B / be the same parts of the number / C D / that / A E / subtracted is of / C F / subtracted

construct cut_equal_segment(/ A B /) → / G H / (equal)

assert whatever parts / G H / is of / C D /, the same parts also is / A E / of / C F /

assert Let / G H / be divided into the parts of / C D /, namely / G K /, / K H /, and / A E / into the parts of / C F /, namely / A L /, / L E /

assert the multitude of / G K /, / K H / will be equal to the multitude of / A L /, / L E /

assert Now since, whatever part / G K / is of / C D /, the same part also is / A L / of / C F /, while / C D / > / C F /,

assert / G K / is also greater than / A L /

construct cut_equal_segment(/ A L /) → / G M / (equal)

assert whatever part / G K / is of / C D /, the same part also is / G M / of / C F /

∵ number_part_number_vii_7assert also / M K / is the same part of / F D / that / G K / is of / C D /

assert Since, whatever part / K H / is of / C D /, the same part also is / L E / of / C F /, while / C D / > / C F /,

assert / K H / is also greater than / L E /

construct cut_equal_segment(/ L E /) → / K N / (equal)

assert whatever part / K H / is of / C D /, the same part also is / K N / of / C F /

∵ number_part_number_vii_7assert also / N H / is the same part of / F D / that / K H / is of / C D /

assert / M K / was also proved to be the same part of / F D / that / G K / is of / C D /

assert also the sum of / M K /, / N H / is the same parts of / F D / that / G H / is of / C D /

assert The sum of / M K /, / N H / is equal to / E B /, and / G H / = / A B /

∴ / E B / is the same parts of / F D / that / A B / is of / C D /

Dependency Graph

Required for

G.264, G.368, G.370