A formal exploration of constructive geometry
Main page  ## Proposition 5

In isosceles triangles the angles at the base are equal to one another, and, if the equal straight lines be produced further, the angles under the base will be equal to one another.

This proposition proves that if we have an isosceles triangle from which lines are extended from the base, then the angles under the base will be equal as well.

We can see that this is obvious due to the properties of supplemental angles, however Euclid doesn't prove this property until Proposition 13, so we can not take it for granted here. Euclid proves this by extending lines from the base of the isosceles triangle and then taking a point from each extended line such that the length of the segments created are equal, BF and CG below. The points taken from the line are connected to the opposite side of the base of the isosceles triangle. The triangles that are created can be proved congruent by SAS and therefore we can say that their respective angles are congruent.

Only points B and F can be moved in this diagram. A is anchored and C and G are mirrored from B and F to maintain the isosceles and equivalent length properties.

 div.scroll { overflow: scroll; width:350px; height:500px; overflow-x: hidden; } .tooltip1 { position: relative; display: inline-block; border-bottom: 1px dotted black; } .tooltip1 .tooltiptext1 { visibility: hidden; width: 120px; background-color: white; color: black; text-align: center; border-radius: 3px; padding: 5px 0; border-style: solid; border-color: black; border-width: 1px; /* Position the tooltip */ position: absolute; z-index: 1; } .tooltip1:hover .tooltiptext1 { visibility: visible; } Let ABC be an isosceles triangle having the side AB equal to the side AC; And let the straight lines BD, CE be produced further in a straight line with AB, AC. [Post.2]To produce a finite straight line continuously in a straight line. I say that the angle ABC is equal to the angle ACB, and the angle CBD to the angle BCE. Let a point F be taken at random on BD; from AE the greater let AG be cut off equal to AF the less; [1.3]Given two unequal straight lines, to cut off the greater a straight line equal to the less.and let the straight lines FC, GB be joined. [Post.1]To draw a straight line from any point to any point. Then, since AF is equal to AG and AB to AC, the two sides FA, AC are equal to the two sides GA, AB, respectively; and they contain a common angle, the angle FAG. Therefore the base FC is equal to the base GB, and the triangle AFC is equal to the triangle AGB, and the remaining angles will be equal to the remaining angles respectively, namely those which the equal sides subtend, that is, the angle ACF to the angle ABG, and the angle AFC to the angle AGB. [1.4](S.A.S.) If two triangles have the sides equal to two sides respectively, and have the angles contained by the equal straight lines equal, they will also have the base equal to the base, the triangle will be equal to the triangle, and the remaining angles respectively, namely those which the equal sides subtend. And, since the whole AF is equal to the whole AG, and in these AB is equal to AC, the remainder BF is equal to the remainder CG. But FC was also proved equal to GB; therefore the two sides BF, FC are equal to the two sides CG, GB respectively; and the angle BFC is equal to the angle CGB, while the base BC is common to them; therefore the triangle BFC is also equal to the triangle CGB, and the remaining angles will be equal to the remaining angles respectively, namely those which the equal sides subtend; therefore the angle FBC is equal to the angle GCB, and the angle BCF to the angle CBG. Accordingly, since the whole angle ABG was proved equal to the angle ACF, and in these the angle CBG is equal to the angle BCF, the remaining angle ABC is equal to the remaining angle ACB; and they are at the base of the triangle ABC. But the angle FBC was also proved equal to the angle GCB; and they are under the base. Therefore etc; Q. E. D.

### Proof in Nuprl

In the Nuprl proof we use the variable j instead of F, and k instead of G.  Index