Rules of derivation
What may license a step. A proposition of Euclid enters this table only after its wording has been compared with the page of Heath's translation (1908); lemmas are the author's and say what they rest on. The conditions are what a proposition takes from the figure: they are evaluated in every configuration.
| rule | statement | from | to | what the figure must supply | locus |
|---|---|---|---|---|---|
| Elements I.13 proposition | If a straight line set up on a straight line make angles, it will make either two right angles or angles equal to two right angles. | — | equal(angle(P, V, X) + angle(X, V, Q), 180°) | collinear(P, V, Q)between(V, P, Q)distinct(V, X) | Heath, vol. I, p. 275 |
| Elements I.28 proposition | If a straight line falling on two straight lines make the exterior angle equal to the interior and opposite angle on the same side, or the interior angles on the same side equal to two right angles, the straight lines will be parallel to one another. | equal(angle(T1, V1, P), angle(T2, V2, Q)) | parallel(line(V1, P), line(V2, Q)) | distinct(V1, V2)collinear(T1, V1, V2)collinear(T2, V1, V2)same_direction(V1, T1, V2, T2)same_side(P, Q, V1, V2) | Heath, vol. I, p. 309 |
| Elements I.29 proposition | A straight line falling on parallel straight lines makes the alternate angles equal to one another, the exterior angle equal to the interior and opposite angle, and the interior angles on the same side equal to two right angles. | parallel(line(P, Q), line(R, S)) | equal(angle(P, Q, R), angle(Q, R, S)) | distinct(Q, R)opposite_side(P, S, Q, R) | Heath, vol. I, p. 311 |
| Elements I.30 proposition | Straight lines parallel to the same straight line are also parallel to one another. | parallel(line(A, B), line(M, N))parallel(line(C, D), line(M, N)) | parallel(line(A, B), line(C, D)) | — | Heath, vol. I, p. 314 |
| Elements I.32 proposition | In any triangle, if one of the sides be produced, the exterior angle is equal to the two interior and opposite angles, and the three interior angles of the triangle are equal to two right angles. | — | equal(angle(A, C, D), angle(C, A, B) + angle(A, B, C)) | noncollinear(A, B, C)collinear(B, C, D)between(C, B, D) | Heath, vol. I, p. 316 |
| Elements I.33 proposition | The straight lines joining equal and parallel straight lines (at the extremities which are) in the same directions (respectively) are themselves also equal and parallel. | parallel(line(A, B), line(C, D))equal(distance(A, B), distance(C, D)) | parallel(line(A, C), line(B, D))equal(distance(A, C), distance(B, D)) | same_direction(A, B, C, D)noncollinear(A, B, C) | Heath, vol. I, p. 322 |
| Elements I.34 proposition | In parallelogrammic areas the opposite sides and angles are equal to one another, and the diameter bisects the areas. | parallel(line(A, B), line(C, D))parallel(line(A, C), line(B, D)) | equal(distance(A, B), distance(C, D))equal(distance(A, C), distance(B, D)) | noncollinear(A, B, C) | Heath, vol. I, p. 323 |
| Elements I.47 proposition | In right-angled triangles the square on the side subtending the right angle is equal to the squares on the sides containing the right angle. | perpendicular(line(X, F), line(Y, Z)) | equal(distance(X, Y) * distance(X, Y), distance(X, F) * distance(X, F) + distance(Y, F) * distance(Y, F)) | collinear(Y, Z, F)distinct(Y, F)distinct(X, F) | Heath, vol. I, p. 349 |
| Elements VI.6 proposition | If two triangles have one angle equal to one angle and the sides about the equal angles proportional, the triangles will be equiangular and will have those angles equal which the corresponding sides subtend. | equal(angle(B, A, C), angle(E, D, F))equal(distance(A, B) / distance(A, C), distance(D, E) / distance(D, F)) | equal(angle(A, B, C), angle(D, E, F))equal(angle(A, C, B), angle(D, F, E)) | noncollinear(A, B, C)noncollinear(D, E, F) | Heath, vol. II, p. 204 |
| lemma same ray lemma | Two points that lie from a point C in the same direction along parallels to one line, at equal distances from C, coincide. | parallel(line(C, X), line(M, N))parallel(line(C, Y), line(M, N))equal(distance(C, X), distance(C, Y)) | coincident(X, Y) | same_direction(C, X, C, Y) | Elements I.30 (the two parallels through C are one line) and the uniqueness of the point cut off on a ray at a given distance (I.3) |
| lemma same angle lemma | Two points that subtend equal angles with a ray VP at V and lie on the same side of it are seen from V in the same direction. | equal(angle(P, V, X), angle(P, V, Y)) | equal(direction(V, X), direction(V, Y)) | distinct(V, P)same_side(X, Y, V, P) | the uniqueness of the angle constructed on a given side of a line at a point (Elements I.23, with Common Notion 5 as in the proof of I.7) |
| lemma segment addition lemma | If B lies between A and C on one line, AC is AB and BC together. | — | equal(distance(A, C), distance(A, B) + distance(B, C)) | collinear(A, B, C)between(B, A, C) | Common Notion 4 (things which coincide are equal) with the definition of a whole and its parts; the configuration is the hypothesis |
| lemma one line lemma | Three points on one line give lines from one of them to the other two that are parallel (they are one line). | collinear(A, B, C) | parallel(line(A, B), line(A, C)) | distinct(A, B)distinct(A, C) | Definition I.23 read with coincident lines counted as parallel, as the predicate `parallel` does |
| trigonometry sine definition | In a right triangle the side opposite an acute angle is the hypotenuse times the sine of that angle. | perpendicular(line(X, F), line(Y, Z)) | equal(distance(X, F), distance(X, Y) * sin(angle(X, Y, F))) | collinear(Y, Z, F)distinct(Y, F)distinct(X, F) | — |
| trigonometry cosine definition | In a right triangle the side adjacent to an acute angle is the hypotenuse times the cosine of that angle. | perpendicular(line(X, F), line(Y, Z)) | equal(distance(Y, F), distance(X, Y) * cos(angle(X, Y, F))) | collinear(Y, Z, F)distinct(Y, F)distinct(X, F) | — |
| trigonometry tangent definition | In a right triangle the tangent of an acute angle is the opposite side over the adjacent side. | perpendicular(line(X, F), line(Y, Z)) | equal(tan(angle(X, Y, F)), distance(X, F) / distance(Y, F)) | collinear(Y, Z, F)distinct(Y, F)distinct(X, F) | — |
| common notion 1 equality | Things which are equal to the same thing are also equal to one another. | — | — | — | Heath, vol. I, p. 155 |
| common notion 5 part | The whole is greater than the part. | — | — | — | Heath, vol. I, p. 155 |
| construction construction | The proposition is read off the cited constructions: it holds for every parameter value and every state without any hypothesis. | — | — | — | — |
| expansion approximation | The two expressions agree to the stated order in a small ratio: their relative difference falls like that power of the ratio. | — | — | — | — |
| cases cases | The claim is reached in every case, and the cases cover every configuration. | — | — | — | — |
| algebra calculation | The proposition follows from the cited equalities by calculation. | — | — | — | — |
