G.455 medial segment there

X.74

If from a medial segment there be subtracted a medial segment which is commensurable with the whole in square only, and which contains with the whole a rational rectangle, the remainder is irrational. And let it be called a first apotome of a medial segment.

medial_segment_there()

prove / A C / is irrational

construct From the medial segment / A B / let there be subtracted the medial segment / B C / which is commensurable with / A B / in square only and with / A B / makes the rectangle / A B /, / B C / rational

assert let it be called a first apotome of a medial segment

assert / A B /, / B C / are medial,

assert The squares on / A B /, / B C / are also medial

assert Twice the rectangle / A B /, / B C / is rational

assert the squares on / A B /, / B C / are incommensurable with twice the rectangle / A B /, / B C /

∵ square_of_difference, incommensurable_magnitudes_addedassert twice the rectangle / A B /, / B C / is also incommensurable with the remainder, the square on / A C /, since, if the whole is incommensurable with one of the magnitudes, the original magnitudes will also be incommensurable

assert Twice the rectangle / A B /, / B C / is rational

∵ square_assigned_segment_def∴ the square on / A C / is irrational; therefore / A C / is irrational

Dependency Graph

Required for

G.462, G.478, G.484, G.490, G.495