Skip to main content
PRL Project




A formal exploration of constructive geometry
Main page

Previous Page Next Page



Proposition 3

Given two unequal straight lines, to cut off from the greater a straight line equal to the less.

This proposition accomplishes subtracting from a given line, a line of shorter length. This construction relies heavily, almost solely, on Proposition 2.

This proof and step-by-step construction may seem almost trivial, or maybe it seems complicated for what we accomplish. This is again another instance in which analytic geometry proves much simpler; we would simply take the measure of length of the shorter of the given lines and cut that length from the longer line. To do this in Euclidean geometry we first construct a circle at center A using a radius of length C, which is given. This ensures that the circle constructed will intersect line AB at a point E since AB is longer than the length C. This is an application of the line-circle property that Euclid takes for granted. Then we know that AE=C1C2 and A_E_B.

Let AB, C be the two given unequal straight lines, and let AB be the greater of them.

Thus it is required to cut off from AB the greater a straight line equal to C the less.

At the point A let AD be placed equal to the straight line C; [1.2]To place at a given point [as an extremity] a straight line equal to a given straight line. and with centre A and distance AD let the circle DEF be described. [Post. 3]To describe a circle with any centre and distance.

Now, since the point A is the centre of the circle DEF, AE is equal to AD. [Def. 15]A circle is a plane figure contained by one line such that all the straight lines falling upon it from one point among those lying within the figure are equal to one another.

But C is also equal to AD. [Def. 15]A circle is a plane figure contained by one line such that all the straight lines falling upon it from one point among those lying within the figure are equal to one another.

Therefore each of the straight lines AE, C is equal to AD; so that AE is also equal to C. [C.N.1]Things which are equal to the same thing are also equal to one another.

Therefore, given the two straight lines AB, C, from AB the greater AE has been cut off equal to C the less.

(Being) what it was required to do.


Proof in Nuprl







Previous Page Next Page


Index


Website feedback
PRL Project   |   Computer Science Department   |   Cornell University
nuprl@cs.cornell.edu   |   320 Gates Hall, Ithaca, NY 14853   |   © 2014 Cornell University
site admin | Prof Constable's Library | PRL SourceForge Project Page