avewright/proofwiki-math huggingface dataset:
Theorem: Cotangent of Sum of Three Angles

:$\map \cot {A + B + C} = \dfrac {\cot A + \cot B + \cot C - \cot A \cot B \cot C} {1 - \cot B \cot C - \cot C \cot A - \cot A \cot B}$

Proof:
{{begin-eqn}}
{{eqn | l = \map \cos {A + B + C}
      | r = \cos A \cos B \cos C - \sin A \sin B \cos C - \sin A \cos B \sin C - \cos A \sin B \sin C
      | c = Cosine of Sum of Three Angles
}}
{{eqn | l = \map \sin {A + B + C}
      | r = \sin A \cos B \cos C + \cos A \sin B \cos C + \cos A \cos B \sin C - \sin A \sin B \sin C
      | c = Sine of Sum of Three Angles
}}
{{eqn | ll= \leadsto
      | l = \map \cot {A + B + C}
      | r = \dfrac {\cos A \cos B \cos C - \sin A \sin B \cos C - \sin A \cos B \sin C - \cos A \sin B \sin C} {\sin A \cos B \cos C + \cos A \sin B \cos C + \cos A \cos B \sin C - \sin A \sin B \sin C}
      | c = Cotangent is Cosine divided by Sine
}}
{{eqn | r = \dfrac {\frac {\cos A \cos B \cos C} {\sin A \sin B \sin C} - \frac {\sin A \sin B \cos C} {\sin A \sin B \sin C} - \frac {\sin A \cos B \sin C} {\sin A \sin B \sin C} - \frac {\cos A \sin B \sin C} {\sin A \sin B \sin C} } {\frac {\sin A \cos B \cos C} {\sin A \sin B \sin C} + \frac {\cos A \sin B \cos C} {\sin A \sin B \sin C} + \frac {\cos A \cos B \sin C} {\sin A \sin B \sin C} - \frac {\sin A \sin B \sin C} {\sin A \sin B \sin C} }
      | c = dividing numerator and denominator by $\sin A \sin B \sin C$
}}
{{eqn | r = \dfrac {\cot A + \cot B + \cot C - \cot A \cot B \cot C} {1 - \cot B \cot C - \cot C \cot A - \cot A \cot B}
      | c = Cotangent is Cosine divided by Sine and simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Cotangents of Half Angles in Triangle

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

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {\cot \frac A 2 + \cot \frac B 2 + \cot \frac C 2 - \cot \frac A 2 \cot \frac B 2 \cot \frac C 2} {1 - \cot \frac B 2 \cot \frac C 2 - \cot \frac C 2 \cot \frac A 2 - \cot \frac A 2 \cot \frac B 2}
      | r = \map \cot {\frac A 2 + \frac B 2 + \frac C 2}
      | c = Cotangent of Sum of Three Angles
}}
{{eqn | r = \cot 90 \degrees
      | c = Sum of Angles of Triangle equals Two Right Angles
}}
{{eqn | r = 0
      | c = Cotangent of Right Angle
}}
{{eqn | ll= \leadsto
      | l = \cot \frac A 2 + \cot \frac B 2 + \cot \frac C 2 - \cot \frac A 2 \cot \frac B 2 \cot \frac C 2
      | r = 0
      | c = multiplying both sides by $1 - \cot \dfrac B 2 \cot \dfrac C 2 - \cot \dfrac C 2 \cot \dfrac A 2 - \cot \dfrac A 2 \cot \dfrac B 2$
}}
{{eqn | ll= \leadsto
      | l = \cot \frac A 2 + \cot \frac B 2 + \cot \frac C 2
      | r = \cot \frac A 2 \cot \frac B 2 \cot \frac C 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Sines of Angles in Triangle

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

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 = \dfrac A 2 + \dfrac {B + C} 2
      | r = 90 \degrees
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \dfrac {B + C} 2
      | r = 90 \degrees - \dfrac A 2
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \sin A + \sin B + \sin C
      | r = \sin A + 2 \map \sin {\dfrac {B + C} 2} \map \cos {\dfrac {B - C} 2}
      | c = Sine plus Sine
}}
{{eqn | r = 2 \sin \dfrac A 2 \cos \dfrac A 2 + 2 \map \sin {\dfrac {B + C} 2} \map \cos {\dfrac {B - C} 2}
      | c = Double Angle Formula for Sine
}}
{{eqn | r = 2 \sin \dfrac A 2 \cos \dfrac A 2 + 2 \map \sin {90 \degrees - \dfrac A 2} \map \cos {\dfrac {B - C} 2}
      | c = from $(1)$
}}
{{eqn | r = 2 \sin \dfrac A 2 \cos \dfrac A 2 + 2 \cos \dfrac A 2 \map \cos {\dfrac {B - C} 2}
      | c = Sine of Complement equals Cosine
}}
{{eqn | r = 2 \cos \dfrac A 2 \paren {\sin \dfrac A 2 + \map \cos {\dfrac {B - C} 2} }
      | c = factorising
}}
{{eqn | r = 2 \cos \dfrac A 2 \paren {\sin \dfrac A 2 + 2 \cos \dfrac B 2 \cos \dfrac C 2 - \map \cos {\dfrac {B + C} 2} }
      | c = Werner Formula for Cosine by Cosine
}}
{{eqn | r = 2 \cos \dfrac A 2 \paren {\sin \dfrac A 2 + 2 \cos \dfrac B 2 \cos \dfrac C 2 - \map \cos {90 \degrees - \dfrac A 2} }
      | c = from $(1)$
}}
{{eqn | r = 2 \cos \dfrac A 2 \paren {\sin \dfrac A 2 + 2 \cos \dfrac B 2 \cos \dfrac C 2 - \sin \dfrac A 2}
      | c = Cosine of Complement equals Sine
}}
{{eqn | r = 4 \cos \dfrac A 2 \cos \dfrac B 2 \cos \dfrac C 2
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Cosines of Angles in Triangle

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

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 = \dfrac {A + B} 2 + \dfrac C 2
      | r = 90 \degrees
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \dfrac {A + B} 2
      | r = 90 \degrees - \dfrac C 2
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \cos A + \cos B + \cos C - 1
      | r = 2 \map \cos {\dfrac {A + B} 2} \map \cos {\dfrac {A - B} 2} + \cos C - 1
      | c = Cosine plus Cosine
}}
{{eqn | r = 2 \map \cos {\dfrac {A + B} 2} \map \cos {\dfrac {A - B} 2} - 2 \sin^2 \dfrac C 2
      | c = {{Corollary|Double Angle Formula for Cosine|5}}
}}
{{eqn | r = 2 \map \cos {90 \degrees - \dfrac C 2} \map \cos {\dfrac {A - B} 2} - 2 \sin^2 \dfrac C 2
      | c = from $(1)$
}}
{{eqn | r = 2 \sin \dfrac C 2 \map \cos {\dfrac {A - B} 2} - 2 \sin^2 \dfrac C 2
      | c = Cosine of Complement equals Sine
}}
{{eqn | r = 2 \sin \dfrac C 2 \paren {\map \cos {\dfrac {A - B} 2} - \sin \dfrac C 2}
      | c = factorising
}}
{{eqn | r = 2 \sin \dfrac C 2 \paren {\map \cos {\dfrac {A - B} 2} - \map \sin {90 \degrees - \dfrac {A + B} 2} }
      | c = from $(1)$
}}
{{eqn | r = 2 \sin \dfrac C 2 \paren {\map \cos {\dfrac {A - B} 2} - \map \cos {\dfrac {A + B} 2} }
      | c = Sine of Complement equals Cosine
}}
{{eqn | r = 2 \sin \dfrac C 2 \paren {2 \sin \dfrac A 2 \sin \dfrac B 2}
      | c = Cosine minus Cosine
}}
{{eqn | r = 4 \sin \dfrac A 2 \sin \dfrac B 2 \sin \dfrac C 2
      | c = simplification
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Solutions of sin x equals sin a

Let $\alpha \in \closedint {-1} 1$ be fixed.
Let:
:$(1): \quad \sin x = \sin \alpha$
The solution set of $(1)$ is:
:$\set {x \in \R: \forall n \in \Z: x = n \pi + \paren {-1}^n \alpha}$

Proof:
From Sine of Supplementary Angle:
:$\map \sin {\pi - x} = \sin x$
and so from Real Sine Function is Periodic:
{{begin-eqn}}
{{eqn | l = x
      | r = 2 n \pi + a
      | c = 
}}
{{eqn | l = x
      | r = \paren {2 n + 1} \pi - a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = n \pi + \paren {-1}^n x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Solutions of cos x equals cos a

Let $\alpha \in \closedint {-1} 1$ be fixed.
Let:
:$(1): \quad \cos x = \cos \alpha$
The solution set of $(1)$ is:
:$\set {x \in \R: \forall n \in \Z: x = 2 n \pi \pm \alpha}$

Proof:
From Cosine of Supplementary Angle:
:$\map \cos {\pi - x} = -\cos x$
and so from Real Cosine Function is Periodic:
{{begin-eqn}}
{{eqn | l = x
      | r = 2 n \pi \pm a
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Solutions of tan x equals tan a

Let $\alpha \in \R$ be fixed.
Let:
:$(1): \quad \tan x = \tan \alpha$
The solution set of $(1)$ is:
:$\set {x \in \R: \forall n \in \Z: x = n \pi + \alpha}$

Proof:
From Tangent Function is Periodic on Reals:
:$\map \tan {\pi + x} = \tan x$
Hence:
{{begin-eqn}}
{{eqn | l = x
      | r = n \pi + a
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Quotient Mapping is Linear Transformation

Let $K$ be a field.
Let $V$ be a vector space over $K$.
Let $M$ be a subspace of $V$.
Let $V / M$ be the quotient vector space.
Let $Q: V \to V / M$ be the quotient mapping.
Then $Q$ is a linear transformation.

Proof:
Let $\lambda, \mu \in K$ and $x, y \in V$.
From Quotient Vector Space is Vector Space, it follows that $V / M$ is a vector space.
Using the definition of vector addition and scalar multiplication for $V/M$, we have: 
{{begin-eqn}}
{{eqn	| l = \map Q {\lambda x + \mu y}
		| r = \paren {\lambda x + \mu y} + M
        | c = Definition of quotient mapping
}}
{{eqn	| r = \paren {\lambda x + M} + \paren {\mu y + M}
}}
{{eqn	| r = \lambda \paren {x + M} + \mu \paren {y + M}
}}
{{eqn	| r = \lambda \map Q x + \mu \map Q y
        | c = Definition of quotient mapping
}}
{{end-eqn}}
{{qed}}
Theorem: Kernel of Quotient Mapping

Let $V$ be a vector space.
Let $M$ be a subspace of $V$.
Let $Q: V \to V / M$ be the quotient mapping.
Then:
:$\ker Q = M$
where $\ker Q$ is the kernel of $Q$.

Proof:
For $v \in V$, we have that:
:$v \in \ker Q$
{{iff}}
:$v + M = 0 + M$
That is, {{iff}}:
:$v \in M$
Hence:
:$\ker Q = M$
{{qed}}
Theorem: Cosine of Half Angle in Triangle

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$.
Let $s$ denote the semiperimeter of $\triangle ABC$.
Then:
:$\cos \dfrac C 2 = \sqrt {\dfrac {s \paren {s - c} } {a b} }$

Proof:
{{begin-eqn}}
{{eqn | l = \cos C
      | r = \dfrac {a^2 + b^2 - c^2} {2 a b}
      | c = Law of Cosines
}}
{{eqn | ll= \leadsto
      | l = 2 \cos^2 \dfrac C 2 - 1
      | r = \dfrac {a^2 + b^2 - c^2} {2 a b}
      | c = {{Corollary|Double Angle Formula for Cosine|1}}
}}
{{eqn | ll= \leadsto
      | l = 2 \cos^2 \dfrac C 2
      | r = \dfrac {a^2 + b^2 - c^2} {2 a b} + 1
      | c = 
}}
{{eqn | r = \dfrac {\paren {a^2 + 2 a b + b^2} - c^2} {2 a b}
      | c = common denominator
}}
{{eqn | r = \dfrac {\paren {a + b}^2 - c^2} {2 a b}
      | c = Square of Sum
}}
{{eqn | r = \dfrac {\paren {a + b + c} \paren {a + b - c} } {2 a b}
      | c = Difference of Two Squares
}}
{{eqn | r = \dfrac {2 s \cdot 2 \paren {s - c} } {2 a b}
      | c = {{Defof|Semiperimeter}}
}}
{{eqn | ll= \leadsto
      | l = \cos^2 \dfrac C 2
      | r = \dfrac {s \paren {s - c} } {a b}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \cos \dfrac C 2
      | r = \sqrt {\dfrac {s \paren {s - c} } {a b} }
      | c = taking square root of both sides
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Half Angle in Triangle

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$.
Let $s$ denote the semiperimeter of $\triangle ABC$.
Then:
:$\sin \dfrac C 2 = \sqrt {\dfrac {\paren {s - a} \paren {s - b} } {a b} }$

Proof:
{{begin-eqn}}
{{eqn | l = \cos C
      | r = \dfrac {a^2 + b^2 - c^2} {2 a b}
      | c = Law of Cosines
}}
{{eqn | ll= \leadsto
      | l = 1 - 2 \sin^2 \dfrac C 2
      | r = \dfrac {a^2 + b^2 - c^2} {2 a b}
      | c = {{Corollary|Double Angle Formula for Cosine|2}}
}}
{{eqn | ll= \leadsto
      | l = 2 \sin^2 \dfrac C 2
      | r = 1 - \dfrac {a^2 + b^2 - c^2} {2 a b}
      | c = rearranging
}}
{{eqn | r = \dfrac {c^2 - \paren {a^2 - 2 a b + b^2} } {2 a b}
      | c = common denominator and rearranging
}}
{{eqn | r = \dfrac {c^2 - \paren {a - b}^2} {2 a b}
      | c = Square of Sum
}}
{{eqn | r = \dfrac {\paren {c + a - b} \paren {c - a + b} } {2 a b}
      | c = Difference of Two Squares and simplifying
}}
{{eqn | r = \dfrac {2 \paren {s - b} \cdot 2 \paren {s - a} } {2 a b}
      | c = {{Defof|Semiperimeter}}
}}
{{eqn | ll= \leadsto
      | l = \sin^2 \dfrac C 2
      | r = \dfrac {\paren {s - a} \paren {s - b} } {a b}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \sin\dfrac C 2
      | r = \sqrt {\dfrac {\paren {s - a} \paren {s - b} } {a b} }
      | c = taking square root of both sides
}}
{{end-eqn}}
{{qed}}
Theorem: Tangent of Half Angle in Triangle

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$.
Let $s$ denote the semiperimeter of $\triangle ABC$:
:$s = \dfrac {a + b + c} 2$
Then:
:$\tan \dfrac C 2 = \sqrt {\dfrac {\paren {s - a} \paren {s - b} } {s \paren {s - c} } }$

Proof:
{{begin-eqn}}
{{eqn | l = \tan \dfrac C 2
      | r = \dfrac {\sin \dfrac C 2} {\cos \dfrac C 2}
      | c = 
}}
{{eqn | r = \dfrac {\sqrt {\dfrac {\paren {s - a} \paren {s - b} } {a b} } } {\sqrt {\dfrac {s \paren {s - c} } {a b} } }
      | c = Sine of Half Angle in Triangle, Cosine of Half Angle in Triangle
}}
{{eqn | r = \sqrt {\dfrac {\paren {s - a} \paren {s - b} } {s \paren {s - c} } }
      | c = after simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Condition for Mapping from Quotient Vector Space to be Well-Defined

Let $V, W$ be vector spaces.
Let $T: V \to W$ be a linear transformation.
Let $M$ be a subspace of $V$.
Let $V / M$ be the quotient vector space of $V$ by $M$.
Let $Q_M: V \to V / M$ be the associated quotient mapping.
Then:
:there exists a linear transformation $L: V / M \to W$ such that $L \circ Q_M = T$
{{iff}}:
:$M \subseteq \ker T$
::$\begin {xy} \xymatrix@L + 2mu@ + 1em {V \ar[r]^*{T} \ar[d]_*{Q_M} & W \\ V / M \ar@{-->}[ur]_*{L} } \end {xy}$

Proof:
By Condition for Mapping from Quotient Set to be Well-Defined, it follows that:
:$L: V / M \to W$ exists
{{iff}}
:$\forall v, v' \in V: v + M = v' + M \implies T v = T v'$
Now $v + M = v' + M$ {{iff}} $v - v' \in M$.
We are given that $T$ is a linear transformation, so:
:$T v = T v' \iff T \paren{ v - v' } = 0$
In particular then, with $v' = 0$ it follows that:
:$L: V / M \to W$ exists
{{iff}}
:$\forall v \in V: v \in M \implies T v = 0$
and the latter states that $M \subseteq \ker T$.
{{qed}}
Theorem: Distance from Vertex of Triangle to Orthocenter

Let $\triangle ABC$ be a triangle with sides $a$, $b$ and $c$ opposite vertices $A$, $B$ and $C$ respectively.
Let $H$ be the orthocenter of $\triangle ABC$.
Then:
:$AH = 2 R \size {\cos A}$
where $R$ denotes the circumradius of $\triangle ABC$.

Proof:
:400px
We construct the circumcircle of $\triangle ABC$, whose circumcenter is $K$ and whose circumradius is $R$.
We construct the orthocenter $H$ of $\triangle ABC$ as the intersection of the altitudes $AD$ and $BE$.
First we note the following:
{{begin-eqn}}
{{eqn | l = \angle ABH
      | r = \angle ABE
      | c = 
}}
{{eqn | r = 180 \degrees - \angle AEB - \angle EAB
      | c = Sum of Angles of Triangle equals Two Right Angles
}}
{{eqn | r = 180 \degrees - 90 \degrees - \angle EAB
      | c = by construction
}}
{{eqn | n = 1
      | r = 90 \degrees - A
      | c = simplifying
}}
{{end-eqn}}
Consider $\Box EHCD$.
$\angle CDH$ and $\angle CEH$ are both right angles.
Hence from Opposite Angles of Cyclic Quadrilateral sum to Two Right Angles, $\Box EHCD$ is a cyclic quadrilateral.
Thus:
{{begin-eqn}}
{{eqn | l = \angle AHB
      | r = \angle EHD
      | c = Two Straight Lines make Equal Opposite Angles
}}
{{eqn | l = \angle EHD + \angle DCE
      | r = 180 \degrees
      | c = Opposite Angles of Cyclic Quadrilateral sum to Two Right Angles
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \angle AHB
      | r = 180 \degrees - C
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \dfrac {AH} {\sin \angle ABH}
      | r = \dfrac {AB} {\sin \angle AHB}
      | c = Law of Sines applied to $\triangle ABH$
}}
{{eqn | ll= \leadsto
      | l = \dfrac {AH} {\map \sin {90 \degrees - A} }
      | r = \dfrac {AB} {\map \sin {180 \degrees - C} }
      | c = from $(1)$ and $(2)$
}}
{{eqn | ll= \leadsto
      | l = \dfrac {AH} {\cos A}
      | r = \dfrac {AB} {\sin C}
      | c = Sine of Complement equals Cosine, Sine of Supplementary Angle
}}
{{eqn | r = 2 R
      | c = Law of Sines applied to $\triangle ABC$
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Gauss Lemma for Riemannian Manifolds

Let $\struct {M, g}$ be a Riemannian manifold.
Let $U = \map {\exp_p} {\map {B_\epsilon} 0 }$ be a geodesic ball centered at $p \in M$.
Let $\partial_r$ be the radial vector field on $U \setminus \set p$, where $\setminus$ denotes the set difference.
Then $\partial_r$ is a unit vector field orthogonal to the geodesic spheres in $U \setminus \set p$.

Proof:
{{ProofWanted}}
{{Namedfor|Carl Friedrich Gauss|cat = Gauss}}
Theorem: Angles of Orthic Triangle of Acute Triangle

Let $\triangle ABC$ be an acute triangle with sides $a$, $b$ and $c$ opposite vertices $A$, $B$ and $C$ respectively.
Let $\triangle DEF$ be the orthic triangle of $\triangle ABC$.
Then the angles of $\triangle DEF$ are $180 \degrees - 2 A$, $180 \degrees - 2 B$ and $180 \degrees - 2 C$.

Proof:
:420px
Let $H$ be the orthocenter of $\triangle ABC$.
The quadrilateral $\Box FHDB$ is cyclic.
That is, $\Box FHDB$ can be circumscribed.
Hence:
{{begin-eqn}}
{{eqn | l = \angle HDF
      | r = \angle HBF
      | c = Angles in Same Segment of Circle are Equal
}}
{{eqn | n = 1
      | r = 90 \degrees - A
      | c = as $\triangle AEB$ is a right triangle
}}
{{end-eqn}}
Similarly, $\Box DHEC$ is also a cyclic quadrilateral.
{{begin-eqn}}
{{eqn | l = \angle HDE
      | r = \angle HCE
      | c = Angles in Same Segment of Circle are Equal
}}
{{eqn | n = 2
      | r = 90 \degrees - A
      | c = as $\triangle AFC$ is a right triangle
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \angle FDE
      | r = \angle HDE + \angle HDF
      | c = by construction
}}
{{eqn | r = 180 \degrees - 2 A
      | c = adding $(1)$ and $(2)$
}}
{{end-eqn}}
The same argument {{mutatis}} can be applied to $B$ and $C$.
Hence the result.
{{qed}}
Theorem: Sides of Orthic Triangle of Acute Triangle

Let $\triangle ABC$ be an acute triangle with sides $a$, $b$ and $c$ opposite vertices $A$, $B$ and $C$ respectively.
Let $\triangle DEF$ be the orthic triangle of $\triangle ABC$.
Then the sides of $\triangle DEF$ are $a \cos A$, $b \cos B$ and $c \cos C$.

Proof:
:420px
Let $H$ be the orthocenter of $\triangle ABC$.
Let $R$ be the circumradius of $\triangle ABC$.
{{begin-eqn}}
{{eqn | l = \dfrac {EF} {\sin A}
      | r = \dfrac {AE} {\sin \angle AFE}
      | c = Law of Sines for $\triangle AFE$
}}
{{eqn | r = \dfrac {c \cos A} {\sin C}
      | c = 
}}
{{eqn | r = 2 R \cos A
      | c = 
}}
{{eqn | ll= \leadsto
      | l = EF
      | r = 2 R \cos A \sin A
      | c = 
}}
{{eqn | r = a \cos A
      | c = 
}}
{{end-eqn}}
{{explain|Not obvious what the justification is of the above steps.}}
The same argument {{mutatis}} can be applied to $DF$ and $DE$.
Hence the result.
{{qed}}
Theorem: Sides of Orthic Triangle of Obtuse Triangle

Let $\triangle ABC$ be an obtuse triangle whose sides are $a$, $b$ and $c$ opposite vertices $A$, $B$ and $C$ respectively.
Let $\angle A$ be the obtuse angle of $\triangle ABC$.
Let $\triangle DEF$ be the orthic triangle of $\triangle ABC$.
Then the sides of $\triangle DEF$ are $-a \cos A$, $b \cos B$ and $c \cos C$.

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: Inradius in Terms of Circumradius

Let $\triangle ABC$ be a triangle whose sides are $a$, $b$ and $c$ opposite vertices $A$, $B$ and $C$ respectively.
Let $r$ denote the inradius of $\triangle ABC$.
Let $R$ denote the circumradius of $\triangle ABC$.
Then:
:$r = 4 R \sin \dfrac A 2 \sin \dfrac B 2 \sin \dfrac C 2$

Proof:
:400px
Let $D$, $E$ and $F$ be the points where the incircle is tangent to the sides $AC$, $AB$ and $CB$ respectively.
Let $s$ denote the semiperimeter of $\triangle ABC$.
From Tangent Points of Incircle in Terms of Semiperimeter:
{{begin-eqn}}
{{eqn | l = AD
      | r = s - a
}}
{{eqn | l = BE
      | r = s - b
}}
{{eqn | l = CF
      | r = s - c
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = r
      | r = AI \sin \dfrac A 2
      | c = {{Defof|Sine of Angle}}
}}
{{eqn | l = \dfrac {AI} {\sin \frac B 2}
      | r = \dfrac c {\sin \angle AIB}
      | c = Law of Sines applied to $\triangle AIB$
}}
{{eqn | r = \dfrac c {\map \sin {180 \degrees - \dfrac {A + B} 2} }
      | c = Sum of Angles of Triangle equals Two Right Angles
}}
{{eqn | r = \dfrac c {\sin \dfrac {A + B} 2}
      | c = Sine of Supplementary Angle
}}
{{eqn | r = \dfrac c {\map \sin {\dfrac {180 \degrees - C} 2} }
      | c = Sum of Angles of Triangle equals Two Right Angles
}}
{{eqn | r = \dfrac c {\cos \frac C 2}
      | c = Sine of Complement equals Cosine
}}
{{eqn | r = \dfrac {2 R \sin C} {\cos \frac C 2}
      | c = Law of Sines applied to $\triangle ABC$
}}
{{eqn | r = \dfrac {2 R \cdot 2 \sin \frac C 2 \cos \frac C 2} {\cos \frac C 2}
      | c = Double Angle Formula for Sine
}}
{{eqn | r = 4 R \sin \frac C 2
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = AI
      | r = 4 R \sin \dfrac B 2 \sin \frac C 2 
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r
      | r = 4 R \sin \dfrac A 2 \sin \dfrac B 2 \sin \frac C 2 
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Exradius of Triangle in Terms of Circumradius

Let $\triangle ABC$ be a triangle whose sides are $a$, $b$ and $c$ opposite vertices $A$, $B$ and $C$ respectively.
Let $\rho_a$ be the exradius of $\triangle ABC$ {{WRT}} $a$.
Let $R$ be the circumradius of $\triangle ABC$.
Then:
:$\rho_a = 4 R \sin \dfrac A 2 \cos \dfrac B 2 \cos \dfrac C 2$

Proof:
:500px
Let $r$ denote the inradius of $\triangle ABC$.
We have:
{{begin-eqn}}
{{eqn | l = r
      | r = 4 R \sin \dfrac A 2 \sin \dfrac B 2 \sin \dfrac C 2
      | c = Inradius in Terms of Circumradius
}}
{{eqn | ll= \leadsto
      | l = \rho_a
      | r = 4 R \sin \dfrac A 2 \map \sin {\dfrac {180 \degrees - B} 2} \map \sin {\dfrac {180 \degrees - C} 2}
      | c = 
}}
{{eqn | r = 4 R \sin \dfrac A 2 \map \sin {90 \degrees - \dfrac B 2} \map \sin {90 \degrees - \dfrac C 2}
      | c = 
}}
{{eqn | r = 4 R \sin \dfrac A 2 \cos \dfrac B 2 \cos \dfrac C 2
      | c = Sine of Complement equals Cosine
}}
{{end-eqn}}
{{explain|Why the second line? From the book it says "It should be noted that this formula can be deduced from Inradius in Terms of Circumradius by writing $\paren {180 \degrees - B}$ for $B$ and $\paren {180 \degrees - C}$ for $C$" but plenty of work is needed to show why this is valid.}}
{{qed}}