avewright/proofwiki-math huggingface dataset:
Theorem: Area of Triangle

This page gathers a variety of formulas for the area of a triangle.

Proof:
:420px
{{begin-eqn}} 
{{eqn | l = \map \Area {ABC}
      | r = \frac 1 2 h c
      | c = Area of Triangle in Terms of Side and Altitude
}}
{{eqn | r = \frac 1 2 h \paren {p + q}
}}
{{eqn | r = \frac 1 2 a b \paren {\frac p a \frac h b + \frac h a \frac q b}
}}
{{eqn | r = \frac 1 2 a b \paren {\sin \alpha \cos \beta + \cos \alpha \sin \beta}
      | c = {{Defof|Sine of Angle}} and {{Defof|Cosine of Angle}}
}}
{{eqn | r = \frac 1 2 a b \, \map \sin {\alpha + \beta}
      | c = Sine of Sum
}}
{{eqn | r = \frac 1 2 a b \sin C
}}
{{end-eqn}}
{{qed}}
Theorem: Area of Triangle

This page gathers a variety of formulas for the area of a triangle.

Proof:
:400px
By definition of sine:
:$h = b \sin C$
From Area of Triangle in Terms of Side and Altitude:
:$\map \Area {ABC} = \dfrac {a h} 2$
Substituting:
:$\map \Area {ABC} = \dfrac {a b \sin C} 2$
{{qed}}
Theorem: Intersecting Chords Theorem

Let $AC$ and $BD$ both be chords of the same circle.
Let $AC$ and $BD$ intersect at $E$.
Then $AE \cdot EC = DE \cdot EB$.

Proof:
:320px
Let $AC$ and $BD$ be intersecting chords of circle $ABCD$.
Let the point of intersection be $E$.
If $E$ is the center of $ABCD$ the solution is trivial, as $AE = EC = BE = ED$ and so $AE \cdot EC = BE \cdot ED$.
Otherwise, let $F$ be the center of $ABCD$.
Let $FG$ be drawn perpendicular to $AC$, and $FH$ be drawn perpendicular to $BD$.
From Conditions for Diameter to be Perpendicular Bisector, $G$ bisects $AC$ and $H$ bisects $BD$.
So $AG = GC$ and $BH = HD$.
From Difference of Two Squares we have that $AE \cdot EC + EG^2 = GC^2$.
Let us add $GF^2$ to these.
So $AE \cdot EC + EG^2 + GF^2 = GC^2 + GF^2$.
But from Pythagoras's Theorem we have that:
:$GC^2 + GF^2 = CF^2$
:$EG^2 + GF^2 = EF^2$
So:
:$AE \cdot EC + EF^2 = CF^2$
Using the same construction, we have that:
:$DE \cdot EB + EF^2 = BF^2$
But $BF = CF$ as both are the radius of the circle $ABCD$.
That gives us:
:$AE \cdot EC + EF^2 = DE \cdot EB + EF^2$
It follows that $AE \cdot EC = DE \cdot EB$
{{Qed}}
Theorem: Intersecting Chords Theorem

Let $AC$ and $BD$ both be chords of the same circle.
Let $AC$ and $BD$ intersect at $E$.
Then $AE \cdot EC = DE \cdot EB$.

Proof:
Join $A$ with $B$ and $C$ with $D$, as shown in this diagram:
:310px
Then we have:
{{begin-eqn}}
{{eqn | l = \angle AEB
      | o = \cong
      | r = \angle DEC
      | c = Two Straight Lines make Equal Opposite Angles
}}
{{eqn | l = \angle BAE
      | o = \cong
      | r = \angle CDE
      | c = Angles in Same Segment of Circle are Equal
}}
{{end-eqn}}
By Triangles with Two Equal Angles are Similar we have $\triangle AEB \sim \triangle DEC$.
Thus:
{{begin-eqn}}
{{eqn | l = \frac {AE} {EB}
      | r = \frac {DE} {EC}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = AE \cdot EC
      | r = DE \cdot EB
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Supremum Plus Constant

Let $S$ be a subset of the set of real numbers $\R$.
Let $S$ be bounded above.
Let $\xi \in \R$.
Then:
:$\ds \map {\sup_{x \mathop \in S} } {x + \xi} = \xi + \map {\sup_{x \mathop \in S} } x$
where $\sup$ denotes supremum.

Proof:
Let $B = \sup S$.
Let $T = \set {x + \xi: x \in S}$.
Since $\forall x \in S: x \le B$ it follows that:
:$\forall x \in S: x + \xi \le B + \xi$
Hence $\xi + B$ is an upper bound for $T$.
If $C$ is the supremum for $T$ then $C \le \xi + B$.
On the other hand:
:$\forall y \in T: y \le C$
Therefore:
:$\forall y \in T: y - \xi \le C - \xi$
Since $S = \set {y - \xi: y \in T}$ it follows that $C - \xi$ is an upper bound for $S$ and so $B \le C - \xi$.
So we have shown that $C \le \xi + B$ and $C \ge \xi + B$, hence the result.
{{qed}}
Theorem: Multiple of Infimum

Let $T \subseteq \R: T \ne \O$ be a non-empty subset of the set of real numbers $\R$.
Let $T$ be bounded below.
Let $z \in \R: z > 0$ be a (strictly) positive real number.
Then:
:$\ds \map {\inf_{x \mathop \in T} } {z x} = z \map {\inf_{x \mathop \in T} } x$
where $\inf$ denotes infimum.

Proof:
From Negative of Infimum is Supremum of Negatives:
:$\ds -\inf_{x \mathop \in T} x = \map {\sup_{x \mathop \in T} } {-x} \implies \inf_{x \mathop \in T} x = -\map {\sup_{x \mathop \in T} } {-x}$
Let $S = \set {x \in \R: -x \in T}$.
From Negative of Infimum is Supremum of Negatives, $S$ is bounded above.
From Multiple of Supremum:
:$\ds \map {\sup_{x \mathop \in S} } {z x} = z \map {\sup_{x \mathop \in S} } x$
Hence:
:$\ds \map {\inf_{x \mathop \in T} } {z x} = -\map {\sup_{x \mathop \in T} } {-z x} = -z \map {\sup_{x \mathop \in T} } {-x} = z \map {\inf_{x \mathop \in T} } x$
{{qed}}
Theorem: Law of Sines

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that $a$ is opposite $A$, $b$ is opposite $B$ and $c$ is opposite $C$.
Then:
:$\dfrac a {\sin A} = \dfrac b {\sin B} = \dfrac c {\sin C} = 2 R$
where $R$ is the circumradius of $\triangle ABC$.

Proof:
Construct the altitude from $B$.
:240px
From the definition of sine:
:$\sin A = \dfrac h c$ and $\sin C = \dfrac h a$
Thus:
:$h = c \sin A$
and:
:$h = a \sin C$
This gives:
:$c \sin A = a \sin C$
So:
:$\dfrac a {\sin A} = \dfrac c {\sin C}$
Similarly, constructing the altitude from $A$ gives:
:$\dfrac b {\sin B} = \dfrac c {\sin C}$
{{qed}}
Theorem: Law of Sines

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that $a$ is opposite $A$, $b$ is opposite $B$ and $c$ is opposite $C$.
Then:
:$\dfrac a {\sin A} = \dfrac b {\sin B} = \dfrac c {\sin C} = 2 R$
where $R$ is the circumradius of $\triangle ABC$.

Proof:
Construct the circumcircle of $\triangle ABC$, let $O$ be the circumcenter and $R$ be the circumradius.
Construct $\triangle AOB$ and let $E$ be the foot of the altitude of $\triangle AOB$ from $O$.
:350px
By the Inscribed Angle Theorem:
:$\angle ACB = \dfrac {\angle AOB} 2$
From the definition of the circumcenter:
:$AO = BO$
From the definition of altitude and the fact that all right angles are congruent:
:$\angle AEO = \angle BEO$
Therefore from Pythagoras's Theorem:
:$AE = BE$
and then from Triangle Side-Side-Side Congruence:
:$\angle AOE = \angle BOE$
Thus:
:$\angle AOE = \dfrac {\angle AOB} 2$
and so:
:$\angle ACB = \angle AOE$
Then by the definition of sine:
:$\sin C = \map \sin {\angle AOE} = \dfrac {c / 2} R$
and so:
:$\dfrac c {\sin C} = 2 R$
The same argument holds for all three angles in the triangle, and so:
:$\dfrac c {\sin C} = \dfrac b {\sin B} = \dfrac a {\sin A} = 2 R$
{{qed}}
Theorem: Law of Sines

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that $a$ is opposite $A$, $b$ is opposite $B$ and $c$ is opposite $C$.
Then:
:$\dfrac a {\sin A} = \dfrac b {\sin B} = \dfrac c {\sin C} = 2 R$
where $R$ is the circumradius of $\triangle ABC$.

Proof:
=== Acute Case ===
Let $\triangle ABC$ be acute.
:400px
Construct the circumcircle of $\triangle ABC$.
Let its radius be $R$.
Construct its diameter $BX$ through $B$.
By Thales' Theorem, $\angle BAX$ is a right angle.
From Angles in Same Segment of Circle are Equal:
:$\angle AXB = \angle ACB$
Then:
{{begin-eqn}}
{{eqn | l = \sin \angle AXB
      | r = \dfrac {AB} {BX}
      | c = {{Defof|Sine of Angle}}
}}
{{eqn | ll= \leadsto
      | l = \sin \angle ACB
      | r = \dfrac c {2 R}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 R
      | r = \dfrac c {\sin C}
      | c = 
}}
{{end-eqn}}
The same construction can be applied to each of the remaining vertices of $\triangle ABC$.
Hence the result.
{{qed|lemma}}
Let $\triangle ABC$ be obtuse.
:400px
As for the acute case, construct the circumcircle of $\triangle ABC$.
Let its radius be $R$.
Construct its diameter $BX$ through $B$.
By Thales' Theorem, $\angle BCX$ is a right angle.
We note that $\Box ABXC$ is a cyclic quadrilateral.
From Opposite Angles of Cyclic Quadrilateral sum to Two Right Angles:
:$\angle BXC = 180 \degrees - A$
Hence using a similar argument to the acute case:
{{begin-eqn}}
{{eqn | l = a
      | r = 2 R \sin \angle BXC
      | c = 
}}
{{eqn | l =
      | r = 2 R \map \sin {180 \degrees - A}
      | c = 
}}
{{eqn | r = 2 R \sin A
      | c = 
}}
{{end-eqn}}
and the result follows.
{{qed}}
Theorem: Law of Sines

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that $a$ is opposite $A$, $b$ is opposite $B$ and $c$ is opposite $C$.
Then:
:$\dfrac a {\sin A} = \dfrac b {\sin B} = \dfrac c {\sin C} = 2 R$
where $R$ is the circumradius of $\triangle ABC$.

Proof:
{{begin-eqn}}
{{eqn | l = \sin b \sin c \cos A
      | r = \cos a - \cos b \cos c
      | c = Spherical Law of Cosines
}}
{{eqn | ll= \leadsto
      | l = \sin^2 b \sin^2 c \cos^2 A
      | r = \cos^2 a - 2 \cos a \cos b \cos c + \cos^2 b \cos^2 c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sin^2 b \sin^2 c \paren {1 - \sin^2 A}
      | r = \cos^2 a - 2 \cos a \cos b \cos c + \cos^2 b \cos^2 c
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = \sin^2 b \sin^2 c - \sin^2 b \sin^2 c \sin^2 A
      | r = \cos^2 a - 2 \cos a \cos b \cos c + \cos^2 b \cos^2 c
      | c = multiplying out
}}
{{eqn | ll= \leadsto
      | l = \paren {1 - \cos^2 b} \paren {1 - \cos^2 c} - \sin^2 b \sin^2 c \sin^2 A
      | r = \cos^2 a - 2 \cos a \cos b \cos c + \cos^2 b \cos^2 c
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = 1 - \cos^2 b - \cos^2 c + \cos^2 b \cos^2 c - \sin^2 b \sin^2 c \sin^2 A
      | r = \cos^2 a - 2 \cos a \cos b \cos c + \cos^2 b \cos^2 c
      | c = multiplying out
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \sin^2 b \sin^2 c \sin^2 A
      | r = 1 - \cos^2 a - \cos^2 b - \cos^2 c + 2 \cos a \cos b \cos c
      | c = rearranging and simplifying
}}
{{end-eqn}}
Let $X \in \R_{>0}$ such that:
:$X^2 \sin^2 a \sin^2 b \sin^2 c = 1 - \cos^2 a - \cos^2 b - \cos^2 c + 2 \cos a \cos b \cos c$
Then from $(1)$:
{{begin-eqn}}
{{eqn | l = \dfrac {X^2 \sin^2 a \sin^2 b \sin^2 c} {\sin^2 b \sin^2 c \sin^2 A}
      | o = =
      | r = \dfrac {1 - \cos^2 a - \cos^2 b - \cos^2 c + 2 \cos a \cos b \cos c} {1 - \cos^2 a - \cos^2 b - \cos^2 c + 2 \cos a \cos b \cos c}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = X^2
      | r = \dfrac {\sin^2 A} {\sin^2 a}
      | c = 
}}
{{end-eqn}}
In a spherical triangle, all of the sides are less than $\pi$ radians.
The same applies to the angles.
From Shape of Sine Function:
:$\sin \theta > 0$ for all $0 < \theta < \pi$
Hence the negative root of $\dfrac {\sin^2 A} {\sin^2 a}$ does not apply, and so:
:$X = \dfrac {\sin A} {\sin a}$
Similarly, from applying the Spherical Law of Cosines to $\cos B$ and $\cos C$:
{{begin-eqn}}
{{eqn | l = \sin a \sin c \cos B
      | r = \cos b - \cos a \cos c
}}
{{eqn | l = \sin a \sin b \cos C
      | r = \cos c - \cos a \cos b
}}
{{end-eqn}}
we arrive at the same point:
{{begin-eqn}}
{{eqn | l = X
      | r = \dfrac {\sin B} {\sin b}
}}
{{eqn | r = \dfrac {\sin A} {\sin a}
}}
{{end-eqn}}
where:
:$X^2 \sin^2 a \sin^2 b \sin^2 c = 1 - \cos^2 a - \cos^2 b - \cos^2 c + 2 \cos a \cos b \cos c$
as before.
Hence we have:
:$\dfrac {\sin a} {\sin A} = \dfrac {\sin b} {\sin B} = \dfrac {\sin c} {\sin C}$
{{qed}}
Theorem: Law of Sines

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that $a$ is opposite $A$, $b$ is opposite $B$ and $c$ is opposite $C$.
Then:
:$\dfrac a {\sin A} = \dfrac b {\sin B} = \dfrac c {\sin C} = 2 R$
where $R$ is the circumradius of $\triangle ABC$.

Proof:
:500px
Let $A$, $B$ and $C$ be the vertices of a spherical triangle on the surface of a sphere $S$.
By definition of a spherical triangle, $AB$, $BC$ and $AC$ are arcs of great circles on $S$.
By definition of a great circle, the center of each of these great circles is $O$.
Let $O$ be joined to each of $A$, $B$ and $C$.
Let $P$ be an arbitrary point on $OC$.
Construct $PQ$ perpendicular to $OA$ meeting $OA$ at $Q$.
Construct $PR$ perpendicular to $OB$ meeting $OB$ at $R$.
In the plane $OAB$:
:construct $QS$ perpendicular to $OA$
:construct $RS$ perpendicular to $OB$
where $S$ is the point where $QS$ and $RS$ intersect.
Let $OS$ and $PS$ be joined.
Let tangents be constructed at $A$ to the arcs of the great circles $AC$ and $AB$.
These tangents contain the spherical angle $A$.
But by construction, $QS$ and $QP$ are parallel to these tangents.
Hence $\angle PQS = \sphericalangle A$.
Similarly, $\angle PRS = \sphericalangle B$.
Also we have:
{{begin-eqn}}
{{eqn | l = \angle COB
      | r = a
}}
{{eqn | l = \angle COA
      | r = b
}}
{{eqn | l = \angle AOB
      | r = c
}}
{{end-eqn}}
It is to be proved that $PS$ is perpendicular to the plane $AOB$.
By construction, $OQ$ is perpendicular to both $PQ$ and $QS$.
Thus $OQ$ is perpendicular to the plane $PQS$.
Similarly, $OR$ is perpendicular to the plane $PRS$.
Thus $PS$ is perpendicular to both $OQ$ and $OR$.
Thus $PS$ is perpendicular to every line in the plane of $OQ$ and $OR$.
That is, $PS$ is perpendicular to the plane $OAB$.
In particular, $PS$ is perpendicular to $OS$, $SQ$ and $SR$
It follows that $\triangle PQS$ and $\triangle PRS$ are right triangles.
From the right triangles $\triangle OQP$ and $\triangle ORP$, we have:
{{begin-eqn}}
{{eqn | n = 1
      | l = PQ
      | r = OP \sin b
}}
{{eqn | n = 2
      | l = PR
      | r = OP \sin a
}}
{{eqn | n = 3
      | l = OQ
      | r = OP \cos b
}}
{{eqn | n = 4
      | l = OR
      | r = OP \cos a
}}
{{end-eqn}}
From the right triangles $\triangle PQS$ and $\triangle PRS$, we have:
{{begin-eqn}}
{{eqn | l = PS
      | r = PS \sin \angle PRS
}}
{{eqn | r = PQ \sin A
}}
{{eqn | l = PS
      | r = PR \sin \angle PRS
}}
{{eqn | r = PR \sin B
}}
{{eqn | ll= \leadsto
      | l = OP \sin b \sin A
      | r = OP \sin a \sin B
      | c = from $(1)$ and $(2)$
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\sin a} {\sin A}
      | r = \dfrac {\sin b} {\sin B}
      | c = 
}}
{{end-eqn}}
The result follows by applying this technique {{mutatis}} to the other angles of $ABC$.
{{qed}}
Theorem: Negative of Supremum is Infimum of Negatives

Let $S$ be a non-empty subset of the real numbers $\R$.
Let $S$ be bounded above.
Then:
:$(1): \quad \set {x \in \R: -x \in S}$ is bounded below
:$(2): \quad \ds -\sup_{x \mathop \in S} x = \map {\inf_{x \mathop \in S} } {-x}$
where $\sup$ and $\inf$ denote the supremum and infimum respectively.

Proof:
As $S$ is non-empty and bounded above, it follows by the Continuum Property that $S$ admits a supremum.
Let $B = \sup S$.
Let $T = \set {x \in \R: -x \in S}$.
By definition, $B$ is an upper bound for $S$.
From Negative of Upper Bound of Set of Real Numbers is Lower Bound of Negatives:
:$-B$ is a lower bound for $T$.
Thus $\set {x \in \R: -x \in S}$ is bounded below.
Let $C$ be the infimum of $T$.
Then by definition of infimum:
:$C \ge -B$
On the other hand:
:$\forall y \in T: y \ge C$
Therefore:
:$\forall y \in T: -y \le -C$
Since $S = \set {x \in \R: -x \in T}$ it follows that $-C$ is an upper bound for $S$.
Therefore $-C \ge B$ and so $C \le -B$.
So $C \le -B$ and $C \ge -B$ and the result follows.
{{qed}}
Theorem: Negative of Infimum is Supremum of Negatives

Let $T$ be a non-empty subset of the real numbers $\R$.
Let $T$ be bounded below.
Then:
:$(1): \quad \set {x \in \R: -x \in T}$ is bounded above
:$(2): \quad \ds -\inf_{x \mathop \in T} x = \map {\sup_{x \mathop \in T} } {-x}$
where $\sup$ and $\inf$ denote the supremum and infimum respectively.

Proof:
As $T$ is non-empty and bounded below, it follows by the Continuum Property that $T$ admits an infimum.
Let $B = \inf T$.
Let $S = \set {x \in \R: -x \in T}$.
Since $\forall x \in T: x \ge B$ it follows that:
:$\forall x \in T: -x \le -B$
Hence $-B$ is an upper bound for $S$, and so $\set {x \in \R: -x \in T}$ is bounded above.
Let $C$ be the supremum of $S$.
Then by definition of supremum:
:$C \le -B$
On the other hand:
:$\forall y \in S: y \le C$
Therefore:
:$\forall y \in S: -y \ge -C$
Since $T = \set {x \in \R: -x \in S}$ it follows that $-C$ is a lower bound for $T$.
Therefore $-C \le B$ and so $C \ge -B$.
So $C \ge -B$ and $C \le -B$ and the result follows.
{{qed}}
Theorem: Infimum Plus Constant

Let $T$ be a subset of the set of real numbers.
Let $T$ be bounded below.
Let $\xi \in \R$.
Then:
:$\ds \map {\inf_{x \mathop \in T} } {x + \xi} = \xi + \map {\inf_{x \mathop \in T} } x$
where $\inf$ denotes infimum.

Proof:
From Negative of Infimum is Supremum of Negatives, we have that:
:$\ds -\inf_{x \mathop \in T} x = \map {\sup_{x \mathop \in T} } {-x} \implies \inf_{x \mathop \in T} x = -\map {\sup_{x \mathop \in T} } {-x}$
Let $S = \set {x \in \R: -x \in T}$.
From Negative of Infimum is Supremum of Negatives, $S$ is bounded above.
We have:
{{begin-eqn}}
{{eqn | l = \map {\sup_{x \mathop \in S} } {x + \xi}
      | r = \xi + \map {\sup_{x \mathop \in S} } x
      | c = Supremum Plus Constant
}}
{{eqn | ll= \leadsto
      | l = \map {\inf_{x \mathop \in T} } {x + \xi}
      | r = -\map {\sup_{x \mathop \in T} } {-x + \xi}
      | c = 
}}
{{eqn | r = \xi - \map {\sup_{x \mathop \in T} } {-x}
      | c = 
}}
{{eqn | r = \xi + \map {\inf_{x \mathop \in T} } x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Infimum of Subset

Let $\struct {U, \preceq}$ be an ordered set.
Let $S \subseteq U$.
Let $T \subseteq S$.
Let $\struct {S, \preceq}$ admit an infimum in $U$.
If $T$ also admits an infimum in $U$, then $\map \inf S \preceq \map \inf T$.

Proof:
Let $B = \map \inf S$.
Then $B$ is a lower bound for $S$.
As $T \subseteq S$, it follows by the definition of a subset that $x \in T \implies x \in S$.
Because $x \in S \implies B \preceq x$ (as $B$ is a lower bound for $S$) it follows that $x \in T \implies B \preceq x$.
So $B$ is a lower bound for $T$.
Therefore $B$ precedes the infimum of $T$ in $U$.
Hence the result.
{{qed}}
Theorem: Construction of Equilateral Triangle

On a given straight line segment, it is possible to construct an equilateral triangle.
{{:Euclid:Proposition/I/1}}

Proof:
As $A$ is the center of circle $BCD$, it follows from {{EuclidDefLink|I|15|Circle}} that $AC = AB$.
As $B$ is the center of circle $ACE$, it follows from {{EuclidDefLink|I|15|Circle}} that $BC = AB$.
So, as $AC = AB$ and $BC = AB$, it follows from {{EuclidCommonNotionLink|1}} that $AC = BC$.
Therefore $AB = AC = BC$.
Therefore $\triangle ABC$ is equilateral.
{{qed}}
{{Euclid Note|1|I}}
Theorem: Construction of Equal Straight Line

At a given point, it is possible to construct a straight line segment of length equal to that of any given straight line segment.
The given point will be an endpoint of the constructed straight line segment.
{{:Euclid:Proposition/I/2}}

Proof:
As $B$ is the center of circle $CGH$, it follows from {{EuclidDefLink|I|15|Circle}} that $BC = BG$.
As $D$ is the center of circle $GKL$, it follows from {{EuclidDefLink|I|15|Circle}} that $DL = DG$.
As $\triangle ABD$ is an equilateral triangle, it follows that $DA = DB$.
Therefore, by {{EuclidCommonNotionLink|3}}, $AL = BG$.
As $AL = BG$ and $BC = BG$, it follows from {{EuclidCommonNotionLink|1}} that $AL = BC$.
Therefore, at the given point $A$, the required straight line segment $AL$ has been placed equal in length to $BC$.
{{qed}}
{{Euclid Note|2|I}}
Theorem: Construction of Equal Straight Lines from Unequal

Given two unequal straight line segments, it is possible to cut off from the greater a straight line segment equal to the lesser.
{{:Euclid:Proposition/I/3}}

Proof:
As $A$ is the center of circle $DEF$, it follows from {{EuclidDefLink|I|15|Circle}} that $AE = AD$.
But $C$ is also equal to $AD$.
So, as $C = AD$ and $AD = AE$, it follows from Common Notion 1 that $AE = C$.
Therefore, given the two straight line segments $AB$ and $C$, from the greater of these $AB$, a length $AE$ has been cut off equal to the lesser $C$.
{{qed}}
{{Euclid Note|3|I}}
Theorem: Triangle Side-Angle-Side Congruence

If $2$ triangles have:
:$2$ sides equal to $2$ sides respectively
:the angles contained by the equal straight lines equal
they will also have:
:their third sides equal
:the remaining two angles equal to their respective remaining angles, namely, those which the equal sides subtend.

Proof:
500px
Let $\triangle ABC$ and $\triangle DEF$ be $2$ triangles having sides $AB = DE$ and $AC = DF$, and with $\angle BAC = \angle EDF$.
If $\triangle ABC$ is placed on $\triangle DEF$ such that:
:the point $A$ is placed on point $D$, and 
:the line $AB$ is placed on line $DE$
then the point $B$ will also coincide with point $E$ because $AB = DE$.
So, with $AB$ coinciding with $DE$, the line $AC$ will coincide with the line $DF$ because $\angle BAC = \angle EDF$.
Hence the point $C$ will also coincide with the point $F$, because $AC = DF$.
But $B$ also coincided with $E$.
Hence the line $BC$ will coincide with line $EF$.
(Otherwise, when $B$ coincides with $E$ and $C$ with $F$, the line $BC$ will not coincide with line $EF$ and two straight lines will enclose a region which is impossible.)
Therefore $BC$ will coincide with $EF$ and be equal to it.
Thus the whole $\triangle ABC$ will coincide with the whole $\triangle DEF$ and thus $\triangle ABC = \triangle DEF$.
The remaining angles on $\triangle ABC$ will coincide with the remaining angles on $\triangle DEF$ and be equal to them.
{{qed}}
{{Euclid Note|4|I}}
Theorem: Isosceles Triangle has Two Equal Angles

In isosceles triangles, the angles at the base are equal to each other.
Also, if the equal straight lines are extended, the angles under the base will also be equal to each other.
{{:Euclid:Proposition/I/5}}

Proof:
200px
Let $\triangle ABC$ be an isosceles triangle whose side $AB$ equals side $AC$.
We extend the straight lines $AB$ and $AC$ to $D$ and $E$ respectively.
Let $F$ be a point on $BD$.
We cut off from $AE$ a length $AG$ equal to $AF$.
We draw line segments $FC$ and $GB$.
Since $AF = AG$ and $AB = AC$, the two sides $FA$ and $AC$ are equal to $GA$ and $AB$ respectively.
They contain a common angle, that is, $\angle FAG$.
So by Triangle Side-Angle-Side Congruence, $\triangle AFC = \triangle AGB$.
Thus $FC = GB$, $\angle ACF = \angle ABG$ and $\angle AFC = \angle AGB$.
Since $AF = AG$ and $AB = AC$, then $BF = CG$.
But $FC = GB$, so the two sides $BF, FC$ are equal to the two sides $CG, GB$ respectively.
Then $\angle BFC = \angle CGB$ while $CB$ is common to both.
Therefore by Triangle Side-Angle-Side Congruence:
:$\triangle BFC = \triangle CGB$
Therefore $\angle FBC = \angle GCB$ and $\angle BCF = \angle CBG$.
So since $\angle ACF = \angle ABG$, and in these $\angle BCF = \angle CBG$, then $\angle ABC = \angle ACB$.
But $\angle ABC$ and $\angle ACB$ are at the base of $\triangle ABC$.
Also, we have already proved that $\angle FBC = \angle GCB$, and these are the angles under the base of $\triangle ABC$.
Hence the result.
{{qed}}
Theorem: Triangle with Two Equal Angles is Isosceles

If a triangle has two angles equal to each other, the sides which subtend the equal angles will also be equal to one another.
Hence, by definition, such a triangle will be isosceles.
{{:Euclid:Proposition/I/6}}

Proof:
:200px
Let $\triangle ABC$ be a triangle in which $\angle ABC = \angle ACB$.
Suppose side $AB$ is not equal to side $AC$. Then one of them will be greater.
{{WLOG}}, Suppose $AB > AC$.
We cut off from $AB$ a length $DB$ equal to $AC$.
We draw the line segment $CD$.
Since $DB = AC$, and $BC$ is common, the two sides $DB, BC$ are equal to $AC, CB$ respectively.
Also, $\angle DBC = \angle ACB$.
So by Triangle Side-Angle-Side Congruence:
:$\triangle DBC = \triangle ACB$
But $\triangle DBC$ is smaller than $\triangle ACB$, which is absurd.
Therefore, have $AB \le AC$. 
A similar argument shows the converse, and hence $AB = AC$.
{{qed}}
Theorem: Triangle with Two Equal Angles is Isosceles

If a triangle has two angles equal to each other, the sides which subtend the equal angles will also be equal to one another.
Hence, by definition, such a triangle will be isosceles.
{{:Euclid:Proposition/I/6}}

Proof:
Let $\angle ABC$ and $\angle ACB$ be the angles that are the same.
{{begin-eqn}}
{{eqn | n = 1
      | l = \angle ABC
      | r = \angle ACB
      | c = {{hypothesis}}
}}
{{eqn | n = 2
      | l = BC
      | r = CB
      | c = Equality is Reflexive
}}
{{eqn | n = 3
      | l = \angle ACB
      | r = \angle ABC
      | c = {{hypothesis}}
}}
{{eqn | n = 4
      | l = \triangle ABC
      | r = \triangle ACB
      | c = Triangle Angle-Side-Angle Congruence by $(1)$, $(2)$ and $(3)$
}}
{{eqn | l = AB
      | r = AC
      | c = from $(4)$
}}
{{end-eqn}}
{{qed}}