avewright/proofwiki-math huggingface dataset:
Theorem: Sum of Cosines of Twice 2 Angles minus Cosine of Twice Third Angle of Triangle

Let $\triangle ABC$ be a triangle.
Then:
:$\cos 2 A + \cos 2 B - \cos 2 C = 1 - 4 \sin A \sin B \cos C$

Proof:
First we note that:
{{begin-eqn}}
{{eqn | l = A + B + C
      | r = 180 \degrees
      | c = Sum of Angles of Triangle equals Two Right Angles
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = A + B
      | r = 180 \degrees - C
      | c = 
}}
{{end-eqn}}
That is, $C$ is the supplement of $A + B$.
Then:
{{begin-eqn}}
{{eqn | l = \cos 2 A + \cos 2 B - \cos 2 C
      | r = 2 \map \cos {A + B} \map \cos {A - B} - \cos 2 C
      | c = Cosine plus Cosine
}}
{{eqn | r = 2 \map \cos {180 \degrees - C} \map \cos {A - B} - \cos 2 C
      | c = from $(1)$
}}
{{eqn | r = -2 \cos C \map \cos {A - B} - \cos 2 C
      | c = Cosine of Supplementary Angle
}}
{{eqn | r = -2 \cos C \paren {\cos A \cos B + \sin A \sin B} - \cos 2 C
      | c = Cosine of Difference
}}
{{eqn | r = -2 \cos C \paren {\cos A \cos B + \sin A \sin B} - \paren {2 \cos^2 C - 1}
      | c = {{Corollary|Double Angle Formula for Cosine|1}}
}}
{{eqn | r = 1 - 2 \sin A \sin B \cos C - 2 \paren {\cos A \cos B + \cos C} \cos C
      | c = multiplying out and rearranging
}}
{{eqn | r = 1 - 2 \sin A \sin B \cos C - 2 \paren {\cos A \cos B + \map \cos {180 \degrees - \paren {A + B} } } \cos C
      | c = from $(1)$
}}
{{eqn | r = 1 - 2 \sin A \sin B \cos C - 2 \paren {\cos A \cos B - \map \cos {A + B} } \cos C
      | c = Cosine of Supplementary Angle
}}
{{eqn | r = 1 - 2 \sin A \sin B \cos C - 2 \paren {\cos A \cos B - \paren {\cos A \cos B - \sin A \sin B} } \cos C
      | c = Cosine of Sum
}}
{{eqn | r = 1 - 2 \sin A \sin B \cos C + 2 \paren {\cos A \cos B - \cos A \cos B} \cos C - 2 \sin A \sin B \cos C
      | c = multiplying out
}}
{{eqn | r = 1 - 4 \sin A \sin B \cos C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Cosines of Twice Angles of Triangle

Let $\triangle ABC$ be a triangle.
Then:
:$\cos 2 A + \cos 2 B + \cos 2 C = -1 - 4 \cos A \cos B \cos C$

Proof:
First we note that:
{{begin-eqn}}
{{eqn | l = A + B + C
      | r = 180 \degrees
      | c = Sum of Angles of Triangle equals Two Right Angles
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = A + B
      | r = 180 \degrees - C
      | c = 
}}
{{end-eqn}}
That is, $C$ is the supplement of $A + B$.
Then:
{{begin-eqn}}
{{eqn | l = \cos 2 A + \cos 2 B + \cos 2 C
      | r = 2 \map \cos {A + B} \map \cos {A - B} + \cos 2 C
      | c = Cosine plus Cosine
}}
{{eqn | r = 2 \map \cos {180 \degrees - C} \map \cos {A - B} + \cos 2 C
      | c = from $(1)$
}}
{{eqn | r = -2 \cos C \map \cos {A - B} + \cos 2 C
      | c = Cosine of Supplementary Angle
}}
{{eqn | r = -2 \cos C \paren {\cos A \cos B + \sin A \sin B} + \cos 2 C
      | c = Cosine of Difference
}}
{{eqn | r = -2 \cos C \paren {\cos A \cos B + \sin A \sin B} + \paren {2 \cos^2 C - 1}
      | c = {{Corollary|Double Angle Formula for Cosine|1}}
}}
{{eqn | r = -1 - 2 \sin A \sin B \cos C + 2 \paren {\cos C - \cos A \cos B} \cos C
      | c = multiplying out and rearranging
}}
{{eqn | r = -1 - 2 \sin A \sin B \cos C + 2 \paren {\map \cos {180 \degrees - \paren {A + B} } - \cos A \cos B} \cos C
      | c = from $(1)$
}}
{{eqn | r = -1 - 2 \sin A \sin B \cos C + 2 \paren {-\map \cos {A + B} - \cos A \cos B} \cos C
      | c = Cosine of Supplementary Angle
}}
{{eqn | r = -1 - 2 \sin A \sin B \cos C + 2 \paren {-\paren {\cos A \cos B - \sin A \sin B} - \cos A \cos B} \cos C
      | c = Cosine of Sum
}}
{{eqn | r = -1 - 2 \sin A \sin B \cos C + 2 \paren {-\cos A \cos B - \cos A \cos B} \cos C + 2 \sin A \sin B \cos C
      | c = multiplying out
}}
{{eqn | r = -1 - 4 \cos A \cos B \cos C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Sines of Twice Angles of Triangle

Let $\triangle ABC$ be a triangle.
Then:
:$\sin 2 A + \sin 2 B + \sin 2 C = 4 \sin A \sin B \sin C$

Proof:
First we note that:
{{begin-eqn}}
{{eqn | l = A + B + C
      | r = 180 \degrees
      | c = Sum of Angles of Triangle equals Two Right Angles
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = A + B
      | r = 180 \degrees - C
      | c = 
}}
{{end-eqn}}
That is, $C$ is the supplement of $A + B$.
Then:
{{begin-eqn}}
{{eqn | l = \sin 2 A + \sin 2 B + \sin 2 C
      | r = 2 \map \sin {A + B} \map \cos {A - B} + \sin 2 C
      | c = Sine plus Sine
}}
{{eqn | r = 2 \map \sin {180 \degrees - C} \map \cos {A - B} + \sin 2 C
      | c = from $(1)$
}}
{{eqn | r = 2 \sin C \map \cos {A - B} + \sin 2 C
      | c = Sine of Supplementary Angle
}}
{{eqn | r = 2 \sin C \paren {\cos A \cos B + \sin A \sin B} + \sin 2 C
      | c = Cosine of Difference
}}
{{eqn | r = 2 \sin C \paren {\cos A \cos B + \sin A \sin B} + 2 \sin C \cos C
      | c = Double Angle Formula for Sine
}}
{{eqn | r = 2 \sin A \sin B \sin C + 2 \paren {\cos C + \cos A \cos B} \sin C
      | c = multiplying out and rearranging
}}
{{eqn | r = 2 \sin A \sin B \sin C + 2 \paren {\map \cos {180 \degrees - \paren {A + B} } + \cos A \cos B} \sin C
      | c = from $(1)$
}}
{{eqn | r = 2 \sin A \sin B \sin C + 2 \paren {-\map \cos {A + B} - \cos A \cos B} \sin C
      | c = Cosine of Supplementary Angle
}}
{{eqn | r = 2 \sin A \sin B \sin C + 2 \paren {-\paren {\cos A \cos B - \sin A \sin B} + \cos A \cos B} \sin C
      | c = Cosine of Sum
}}
{{eqn | r = 2 \sin A \sin B \sin C + 2 \paren {-\cos A \cos B + \cos A \cos B} \sin C + 2 \sin A \sin B \sin C
      | c = multiplying out
}}
{{eqn | r = 4 \sin A \sin B \sin C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Twice Angle minus Sum of Sines of Twice Other Two Angles of Triangle

Let $\triangle ABC$ be a triangle.
Then:
:$\sin 2 A - \sin 2 B - \sin 2 C = -4 \sin A \cos B \cos C$

Proof:
First we note that:
{{begin-eqn}}
{{eqn | l = A + B + C
      | r = 180 \degrees
      | c = Sum of Angles of Triangle equals Two Right Angles
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = A + B
      | r = 180 \degrees - C
      | c = 
}}
{{end-eqn}}
That is, $C$ is the supplement of $A + B$.
Then:
{{begin-eqn}}
{{eqn | l = \sin 2 A - \sin 2 B - \sin 2 C
      | r = 2 \map \cos {A + B} \map \sin {A - B} - \sin 2 C
      | c = Sine minus Sine
}}
{{eqn | r = 2 \map \cos {180 \degrees - C} \map \sin {A - B} - \sin 2 C
      | c = from $(1)$
}}
{{eqn | r = -2 \cos C \map \sin {A - B} - \sin 2 C
      | c = Cosine of Supplementary Angle
}}
{{eqn | r = -2 \cos C \paren {\sin A \cos B - \cos A \sin B} - \sin 2 C
      | c = Sine of Difference
}}
{{eqn | r = -2 \cos C \paren {\sin A \cos B - \cos A \sin B} - 2 \sin C \cos C
      | c = Double Angle Formula for Sine
}}
{{eqn | r = -2 \sin A \cos B \cos C + 2 \paren {\cos A \sin B - \sin C} \cos C
      | c = multiplying out and rearranging
}}
{{eqn | r = -2 \sin A \cos B \cos C + 2 \paren {\cos A \sin B - \map \sin {180 \degrees - \paren {A + B} } } \cos C
      | c = from $(1)$
}}
{{eqn | r = -2 \sin A \cos B \cos C + 2 \paren {\cos A \sin B - \map \sin {A + B} } \cos C
      | c = Sine of Supplementary Angle
}}
{{eqn | r = -2 \sin A \cos B \cos C + 2 \paren {\cos A \sin B - \paren {\sin A \cos B + \cos A \sin B} } \cos C
      | c = Cosine of Sum
}}
{{eqn | r = -2 \sin A \cos B \cos C + 2 \paren {\cos A \sin B - \cos A \sin B} \cos C - 2 \sin A \cos B \cos C
      | c = multiplying out
}}
{{eqn | r = -4 \sin A \cos B \cos C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Cosines of Four Times Angles of Triangle

Let $\triangle ABC$ be a triangle.
Then:
:$\cos 4 A + \cos 4 B + \cos 4 C = 4 \cos 2 A \cos 2 B \cos 2 C - 1$

Proof:
First we note that:
{{begin-eqn}}
{{eqn | l = A + B + C
      | r = 180 \degrees
      | c = Sum of Angles of Triangle equals Two Right Angles
}}
{{eqn | ll= \leadsto
      | l = 2 A + 2 B + 2 C
      | r = 360 \degrees
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = 2 A + 2 B
      | r = 360 \degrees - 2 C
      | c = 
}}
{{end-eqn}}
That is, $2 C$ is the conjugate of $2 A + 2 B$.
Then:
{{begin-eqn}}
{{eqn | l = \cos 4 A + \cos 4 B + \cos 4 C
      | r = 2 \map \cos {2 A + 2 B} \map \cos {2 A - 2 B} + \cos 4 C
      | c = Cosine plus Cosine
}}
{{eqn | r = 2 \map \cos {360 \degrees - 2 C} \map \cos {2 A - 2 B} + \cos 4 C
      | c = from $(1)$
}}
{{eqn | r = 2 \cos 2 C \map \cos {2 A - 2 B} + \cos 4 C
      | c = Cosine of Conjugate Angle
}}
{{eqn | r = 2 \cos 2 C \paren {\cos 2 A \cos 2 B + \sin 2 A \sin 2 B} + \cos 4 C
      | c = Cosine of Difference
}}
{{eqn | r = 2 \cos 2 C \paren {\cos 2 A \cos 2 B + \sin 2 A \sin 2 B} + \paren {2 \cos^2 2 C - 1}
      | c = {{Corollary|Double Angle Formula for Cosine|1}}
}}
{{eqn | r = 2 \cos 2 A \cos 2 B \cos 2 C + 2 \paren {\sin 2 A \sin 2 B + \cos 2 C} \cos 2 C - 1
      | c = multiplying out and rearranging
}}
{{eqn | r = 2 \cos 2 A \cos 2 B \cos 2 C + 2 \paren {\sin 2 A \sin 2 B + \map \cos {360 \degrees - \paren {2 A + 2 B} } } \cos 2 C - 1
      | c = from $(1)$
}}
{{eqn | r = 2 \cos 2 A \cos 2 B \cos 2 C + 2 \paren {\sin 2 A \sin 2 B + \map \cos {2 A + 2 B} } \cos 2 C - 1
      | c = Cosine of Conjugate Angle
}}
{{eqn | r = 2 \cos 2 A \cos 2 B \cos 2 C + 2 \paren {\sin 2 A \sin 2 B + \paren {\cos 2 A \cos 2 B - \sin 2 A \sin 2 B} } \cos C - 1
      | c = Cosine of Sum
}}
{{eqn | r = 2 \cos 2 A \cos 2 B \cos 2 C + 2 \paren {\sin 2 A \sin 2 B - \sin 2 A \sin 2 B} \cos 2 C + 2 \cos 2 A \cos 2 B \cos 2 C - 1
      | c = multiplying out
}}
{{eqn | r = 4 \cos 2 A \cos 2 B \cos 2 C - 1
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Spectrum of Bounded Linear Operator is Closed

Let $\struct {X, \norm \cdot_X}$ be a Banach space over $\C$..
Let $T$ be a bounded linear operator on $X$.
Then the spectrum $\map \sigma T$ of $T$ is a closed set in $\C$.

Proof:
From Resolvent Set of Bounded Linear Operator is Open, the resolvent set $\map \rho T$ is open. 
From the definition of spectrum, we have $\map \sigma T = \C \setminus \map \rho T$.
From the definition of a closed set, $\map \sigma T$ is closed set in $\C$.
{{qed}}
Category:Bounded Linear Operators
Category:Spectra (Bounded Linear Operators)
r247325vw2045raehlmfb7zzu97huq4
Theorem: Length of Angle Bisector in terms of Angle

Let $\triangle ABC$ be a triangle with sides $a$, $b$ and $c$ opposite vertices $A$, $B$ and $C$ respectively.
Let $AD$ be the angle bisector of $\angle BAC$ that intersects $a$ at $D$.
:300px
Then:
:$AD = \dfrac {2 c b \cos \frac A 2} {b + c}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {BD} {DC} 
      | r = \frac c b
      | c = Angle Bisector Theorem
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = BD
      | r = \frac {a c} {b + c}
      | c = as $a = BD + DC$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \frac {AD} {\sin B}
      | r = \frac {BD} {\sin \frac A 2}
      | c = applying Law of Sines to $\triangle ADB$
}}
{{eqn | r = \frac {a c} {\paren {b + c} \sin \frac A 2}
      | c = substituting for $BD$ from $(1)$
}}
{{eqn | ll= \leadsto
      | l = AD
      | r = \frac {a c \sin B} {\paren {b + c} \sin \frac A 2}
      | c = rearranging
}}
{{eqn | r = \frac {c b \sin A} {\paren {b + c} \sin \frac A 2}
      | c = Law of Sines
}}
{{eqn | r = \frac {2 c b \sin \frac A 2 \cos \frac A 2} {\paren {b + c} \sin \frac A 2}
      | c = Double Angle Formula for Sine
}}
{{eqn | r = \frac {2 c b \cos \frac A 2} {b + c}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Construction of Excircle to Triangle

It is possible to construct an excircle to a triangle tangent to any of its three sides.

Proof:
We have that $\angle XBE = \angle CBE$ and $\angle BQE = \angle BRE$, a right angle, and $BE$ is common.
So from Triangle Angle-Side-Angle Congruence we have that $\triangle EQB = \triangle ERB$.
So $EQ = ER$.
For the same reason $ER = EP$.
So $EQ = ER = EP$.
So the circle drawn with radius $ER$ will pass through $P, Q$ and $R$.
From Line at Right Angles to Diameter of Circle it follows that $AX, AY, BC$ are tangent to the circle $PQR$.
Hence the result.
{{qed}}
Category:Excircles of Triangles
n4hdsy2b7szt0ezavvheyleubdgia33
Theorem: Excenters and Incenter of Orthic Triangle/Acute Triangle

Let $\triangle ABC$ be an acute triangle.
Let $\triangle DEF$ be the orthic triangle of $\triangle ABC$ such that:
:$D$ is on $BC$
:$E$ is on $AC$
:$F$ is on $AB$
Then:
:the excenter of $\triangle DEF$ {{WRT}} $EF$ is $A$
:the excenter of $\triangle DEF$ {{WRT}} $DF$ is $B$
:the excenter of $\triangle DEF$ {{WRT}} $DE$ is $C$
and:
:the incenter of $\triangle DEF$ is the orthocenter of $\triangle ABC$.

Proof:
:420px
From Altitudes of Triangle Bisect Angles of Orthic Triangle, $AD$ is the angle bisector of $\angle FDE$.
From Bisectors of Adjacent Angles between Straight Lines Meeting at Point are Perpendicular, the angle bisector of $\angle PDE$ is perpendicular to $AD$.
The line perpendicular to $AD$ is $BC$.
Similarly, from Altitudes of Triangle Bisect Angles of Orthic Triangle, $BE$ is the angle bisector of $\angle FED$.
From Bisectors of Adjacent Angles between Straight Lines Meeting at Point are Perpendicular, the angle bisector of $\angle DEQ$ is perpendicular to $BE$.
The line perpendicular to $BE$ is $AC$.
From Construction of Excircle to Triangle, the intersection of $AC$ and $BC$ is the excenter of $\triangle DEF$ {{WRT}} $DE$.
The same argument can be used {{mutatis}} to demonstrate the locations of the excenter of $\triangle DEF$ {{WRT}} $DF$ and $EF$.
{{qed|lemma}}
:380px
From Altitudes of Triangle Bisect Angles of Orthic Triangle:
:$AD$ is the angle bisector of $\angle FDE$
:$BE$ is the angle bisector of $\angle DEF$
:$FC$ is the angle bisector of $\angle EFD$
From Line from Vertex of Triangle to Incenter is Angle Bisector it follows that $H$ is the incenter of $\triangle DEF$.
{{qed}}
Category:Excenters and Incenter of Orthic Triangle
pv56cglv48p6rr9l7eo5y1f8d9hrtke
Theorem: Orthic Triangle of Obtuse Triangle

Let $\triangle ABC$ be an obtuse triangle such that $A$ is the obtuse angle.
Let $H$ be the orthocenter of $\triangle ABC$.
Let $\triangle DEF$ be the orthic triangle of $\triangle ABC$.
Then $\triangle DEF$ is also the orthic triangle of $\triangle HBC$, which is an acute triangle.

Proof:
:420px
By construction:
:$CE \perp BH$
:$BF \perp CH$
:$HD \perp BC$
Thus by definition $CE$, $BF$ and $HD$ are the altitudes of $\triangle HBC$.
Also by construction, $A$ lies on $CE$, $BF$ and $HD$.
Hence $\triangle DEF$ is the orthic triangle of $\triangle HBC$.
{{finish|Demonstrate that $\triangle HBC$ is acute}}
Category:Orthic Triangles
Category:Obtuse Triangles
axdnkgeax87h2bbpw5d36pjykwlnt14
Theorem: Orthic Triangle of Obtuse Triangle

Let $\triangle ABC$ be an obtuse triangle such that $A$ is the obtuse angle.
Let $H$ be the orthocenter of $\triangle ABC$.
Let $\triangle DEF$ be the orthic triangle of $\triangle ABC$.
Then $\triangle DEF$ is also the orthic triangle of $\triangle HBC$, which is an acute triangle.

Proof:
:420px
Let $H$ be the orthocenter of $\triangle ABC$.
{{begin-eqn}}
{{eqn | l = \frac {EF} {\sin \angle EAF}
      | r = \frac {AF} {\sin \angle AEF}
      | c = Law of Sines for $\triangle AFE$
}}
{{eqn | ll= \leadsto
      | l = \frac {EF} {\sin A}
      | r = \frac {b \map \cos {180 \degrees - A} } {\sin B}
      | c = Angles in Same Segment of Circle are Equal: $BEFC$ is cyclic
}}
{{eqn | r = \frac {a \map \cos {180 \degrees - A} } {\sin A}
      | c = Law of Sines for $\triangle ABC$
}}
{{eqn | ll= \leadsto
      | l = EF
      | r = a \map \cos {180 \degrees - A}
      | c = 
}}
{{eqn | r = -a \cos A
      | c = Cosine of Supplementary Angle
}}
{{end-eqn}}
On the other hand, 
{{begin-eqn}}
{{eqn | l = \frac {DE} {\sin \angle DAE}
      | r = \frac {AD} {\sin \angle AED}
      | c = Law of Sines for $\triangle ADE$
}}
{{eqn | ll= \leadsto
      | l = \frac {DE} {\map \sin {90 \degrees + C} }
      | r = \frac {b \sin C} {\sin B}
      | c = Angles in Same Segment of Circle are Equal: $BEAD$ is cyclic
}}
{{eqn | r = \frac {c \sin C} {\sin C}
      | c = Law of Sines for $\triangle ABC$
}}
{{eqn | ll= \leadsto
      | l = DE
      | r = c \map \sin {90 \degrees + C}
      | c = 
}}
{{eqn | r = c \cos C
      | c = Sine of Angle plus Right Angle
}}
{{end-eqn}}
Similar arguments {{mutatis}} can be applied to $DF$ by swapping $E$ with $F$ and $B$ with $C$.
Hence the result.
{{qed}}
Theorem: Pedal Triangle of Point on Circumcircle is Straight Line

Let $\triangle ABC$ be a triangle.
Let $P$ be an arbitrary point on the circumcircle of $\triangle ABC$.
The pedal triangle of $\triangle ABC$ {{WRT}} $P$ degenerates to a straight line segment.

Proof:
{{ProofWanted|Z423x5c6: I think we can use Menelau's theorem.}}
Theorem: Line from Vertex of Triangle to Incenter is Angle Bisector

Let $\triangle ABC$ be a triangle.
Let $D$ be a point in the interior of $\triangle ABC$.
Then:
:$AD$ is the angle bisector of $A$
:$BD$ is the angle bisector of $B$
:$CD$ is the angle bisector of $C$
{{iff}}:
:$D$ is the incenter of $\triangle ABC$.

Proof:
:420px
Theorem: Hopf-Rinow Theorem

Let $\struct {M, g}$ be a connected Riemannian manifold.
Then $M$ is metrically complete {{iff}} it is geodesically complete.

Proof:
{{ProofWanted}}
{{Namedfor|Heinz Hopf|name2 = Willi Ludwig August Rinow|cat = Hopf|cat2 = Rinow}}
Theorem: Triangle is Orthic Triangle of Triangle formed from Excenters

Let $\triangle ABC$ be a triangle whose sides are $a$, $b$ and $c$ opposite vertices $A$, $B$ and $C$ respectively.
Let $I$ be the incenter of $\triangle ABC$.
Let $I_a$, $I_b$ and $I_c$ be the excenters of $\triangle ABC$ {{WRT}} $a$, $b$ and $c$ respectively.
Let $\triangle I_a I_b I_c$ be the triangle whose vertices are those excenters of $I_a$, $I_b$ and $I_c$.
Then:
:$\triangle ABC$ is the orthic triangle of $\triangle I_a I_b I_c$
and:
:$I$ is the orthocenter of $\triangle I_a I_b I_c$.

Proof:
:560px
From Construction of Excircle to Triangle, it is seen that:
:$A I_b$ is the angle bisector of $\angle PAC$
:$A I_c$ is the angle bisector of $\angle QAB$.
Hence $I_b A I_c$ is a straight line.
From the construction in Excenters and Incenter of Orthic Triangle, $A I I_a$ is a straight line which is perpendicular to $I_b A I_c$.
The same argument {{mutatis}} is used to show that:
:$B I I_b$ is a straight line which is perpendicular to the straight line $I_a B I_c$
and
:$C I I_c$ is a straight line which is perpendicular to the straight line $I_a C I_b$.
It follows by definition that :
:$\triangle ABC$ is the orthic triangle of $\triangle I_a I_b I_c$
and:
:$I$ is the orthocenter of $\triangle I_a I_b I_c$.
{{qed}}
Theorem: Angle Bisectors are Locus of Points Equidistant from Lines

Let $\LL_1$ and $\LL_2$ be straight lines in the plane.
The locus of points which are equidistant from $\LL_1$ and $\LL_2$ are the angle bisectors of $\LL_1$ and $\LL_2$.

Proof:
Let $A'SA$ and $B'SB$ be the straight lines $\LL_1$ and $\LL_2$ respectively, intersecting at the point $S$.
Let $E$ denote the set of points equidistant from both $\LL_1$ and $\LL_2$.
Let $F$ denote the set of points on the angle bisectors of $\LL_1$ and $\LL_2$.
We are to show that $E = F$.
:500px
First we show that $F \subseteq E$.
Let $P \in F$.
{{WLOG}}, let $P$ be on the angle bisector of $\angle ASB$.
Drop perpendiculars $PM$ from $P$ to $SA$ and $PN$ from $P$ to $SB$.
Because:
:$\angle PSM = \angle PSN$
:$\angle PMS = \angle PNS$
:$PS$ is common
we have that:
:$\triangle PSM = \triangle PSN$
and so:
:$PM = PN$
That is, $P$ is equidistant from both $\LL_1$ and $\LL_2$ and so:
:$P \in E$
The same argument is used {{mutatis}} to show that an arbitrary point $P'$ on the angle bisector of $\angle ASB'$ is also equidistant from both $\LL_1$ and $\LL_2$.
That is:
:$P' \in E$
Hence:
:$F \subseteq E$
{{qed|lemma}}
We see immediately that $S \in E$.
As $S$ is on the intersection of $\LL_1$ and $\LL_2$, $S$ is also on their angle bisectors.
Hence $S \in F$.
Let $P \in E$ such that $P \ne S$.
We note that $P \notin \LL_1$ and $P \notin \LL_2$ as that would mean trivially that $P \notin E$.
Drop perpendiculars $PM$ from $P$ to $SA$ and $PN$ from $P$ to $SB$.
With reference to the diagram, note that:
:$PN = PM$
:$\angle PMS = \angle PNS = 90 \degrees$
:$PS$ is common
By Pythagoras's Theorem:
:$SN^2 + PN^2 = PS^2 = SM^2 + PM^2$
But as $PM = PN$ it follows that:
:$SM = SN$
Thus $\triangle PSM$ and $\triangle PSN$ are congruent.
This means:
:$\angle PSN = \angle PSM$
and so $P$ is on one of the angle bisectors of $\LL_1$ and $\LL_2$.
That is:
:$P \in F$
Hence by definition of subset:
:$E \subseteq F$
{{qed|lemma}}
We have:
:$E \subseteq F$
and:
:$F \subseteq E$
and so by definition of set equality:
:$E = F$
Hence the result.
{{qed}}
Theorem: Perpendicular Bisector is Locus of Points Equidistant from Endpoints

Let $AB$ be a straight line segment.
The locus of points which are equidistant from $A$ and $B$ is the perpendicular bisector of $AB$.

Proof:
Let $E$ denote the set of points equidistant from $A$ and $B$.
Let $F$ denote the set of points on the perpendicular bisector of $AB$.
We are to show that $E = F$.
:300px
First we show that $F \subseteq E$.
Let $P \in F$.
Hence by definition $P$ is on the perpendicular bisector of $AB$.
Let $C$ be the intersection of $AB$ and the perpendicular bisector.
We have:
:$\angle PCA = \angle PCB = 90 \degrees$
:$AC = CB$
:$PC$ is common
By Pythagoras's Theorem:
:$AP^2 = AC^2 + PC^2 = BC^2 + PC^2 = BP^2$
and so:
:$AP = BP$
That is, $P$ is equidistant from $A$ and $B$, and so:
:$P \in E$
Hence:
:$F \subseteq E$
{{qed|lemma}}
Let $P \in E$ be arbitrary.
That is, let $P$ be equidistant from $A$ and $B$.
Drop a perpendicular $PC$ to $AB$.
We inspect the triangles $\triangle PCA$ and $\triangle PCA$
We have:
:$PA = PB$
:$\angle PCA = \angle PCB = 90 \degrees$
:$PC$ is common
By Pythagoras's Theorem:
:$AC^2 = PA^2 - PC^2$
:$BC^2 = PB^2 - PC^2$
But as $PA = PB$ it follows that:
:$AC = BC$
Thus $PC$ is the perpendicular bisector of $AB$.
That is:
:$P \in F$
Hence by definition of subset:
:$E \subseteq F$
{{qed|lemma}}
We have:
:$E \subseteq F$
and:
:$F \subseteq E$
and so by definition of set equality:
:$E = F$
Hence the result.
{{qed}}
Theorem: Polygon has Salient Angle

Let $P$ be a polygon.
Then $P$ has at least one salient angle.

Proof:
Recall the definition of salient angle:
:A salient angle is an internal angle which is less than $180 \degrees$.
An internal angle which is not a salient angle is a re-entrant angle.
Let $C$ be a circle such that all vertices of $P$ lie within the interior of $C$.
Let $A$ be the vertex of $P$ that has the minimal distance to the circumference of $C$.
If more than one vertex of $P$ has the same minimal distance to the circumference, choose $A$ among them arbitrarily.
Let $\angle A$ denote the internal angle at $A$.
File:PolygonConvexInternalAngle.png
{{AimForCont}} $\angle A$ is a re-entrant angle.
Let $H$ be the point on the circumference of $C$ that lies closest to $A$.
Let $r$ be the line segment with endpoints $A$ and $H$.
Let $t$ be tangent to $C$ at $H$, which can be constructed by Construction of Tangent from Point to Circle.
Let $l$ be the straight line parallel with $t$ through $A$, which can be constructed by Construction of Parallel Line.
Suppose one of the two adjacent sides of $A$ forms an acute or right angle with $r$.
Then that side would either intersect $C$, or have an endpoint that lies closer to $C$ than $A$.
But {{hypothesis}}:
:$P$ lies completely inside $C$
and
:$A$ is the closest vertex of $P$ to $C$.
Hence neither of the two adjacent sides of $A$ forms an acute or right angle with $r$.
It follows that the adjacent sides of $A$ lie on the same side of $l$.
Then $r$ is an intersecting line of the re-entrant angle formed by the two sides.
As $r$ ends in $H$ in the exterior of $P$, it follows that this re-entrant angle is not the internal angle of the vertex $A$.
This contradicts our definition of $A$.
Hence it follows that the internal angle of the vertex $A$ is salient angle.
{{qed}}
Category:Polygons
Category:Internal Angles
k14rpyvv0w41g73ms0ckdus7zg4jmzu