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

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}} the excircle which is tangent to $a$.
Let $s$ be the semiperimeter of $\triangle ABC$.
Then the area $\AA$ of $\triangle ABC$ is given by:
:$\AA = \rho_a \paren {s - a}$

Proof:
:500px
Let $C$ be the excircle of $\triangle ABC$ which is tangent to $a$.
By definition:
:$\rho_a$ is the radius of $C$
:$I_a$ is the center of $C$.
Then we have:
{{begin-eqn}}
{{eqn | l = \AA
      | r = \map \Area {\triangle ABI_a} + \map \Area {\triangle ACI_a} - \map \Area {\triangle CBI_a}
      | c = (see figure above)
}}
{{eqn | r = \frac {c \rho_a} 2 + \frac {b \rho_a} 2 - \frac {a \rho_a} 2
      | c = Area of Triangle in Terms of Side and Altitude
}}
{{eqn | r = \rho_a \frac {b + c + a} 2 - \rho_a a
}}
{{eqn | r = \rho_a s - \rho_a a
      | c = {{Defof|Semiperimeter}}
}}
{{eqn | l = (ABC)
      | r = \rho_a \paren {s - a}
}}
{{end-eqn}}
{{qed}}
Theorem: Complementary Idempotent of Complementary Idempotent is Idempotent

Let $\HH$ be a Hilbert space.
Let $I$ be an identity operator on $\HH$.
Let $A$ be an idempotent operator.
Let $B$ be the complementary idempotent of A.
Then the complementary idempotent of $B$ is $A$.

Proof:
From Complementary Idempotent is Idempotent the complementary idempotent of $B$ is well-defined.
Let $C$ be the complementary idempotent of $B$.
We have:
{{begin-eqn}}
{{eqn | l = C
      | r = I - B
      | c = {{Defof|Complementary Idempotent}}
}}
{{eqn | r = I - \paren{I - A}
      | c = {{Defof|Complementary Idempotent}}
}}
{{eqn | r = A
}}
{{end-eqn}}
{{qed}}
Category:Linear Transformations on Hilbert Spaces
jmzkexs88f008j8bg6ohkyidom7u96j
Theorem: Complementary Projection of Complementary Projection is Projection

Let $\HH$ be a Hilbert space.
Let $I$ be an identity operator on $\HH$.
Let $A$ be a projection.
Let $B$ be the complementary projection of A.
Then the complementary projection of $B$ is $A$.

Proof:
From Complementary Projection is Projection the complementary projection of $B$ is well-defined.
Let $C$ be the complementary projection of $B$.
We have:
{{begin-eqn}}
{{eqn | l = C
      | r = I - B
      | c = {{Defof|Complementary Projection}}
}}
{{eqn | r = I - \paren{I - A}
      | c = {{Defof|Complementary Projection}}
}}
{{eqn | r = A
}}
{{end-eqn}}
{{qed}}
Category:Linear Transformations on Hilbert Spaces
c4nuz8t30ozjnd7ri2pdomcy14293ss
Theorem: Complementary Projection is Complementary Idempotent

Let $\HH$ be a Hilbert space.
Let $A$ be a projection.
Let $B$ be the complementary projection of A.
Then $B$ is the complementary idempotent of $A$.

Proof:
By the definition of projection, $A$ is an idempotent operator.
The result follows immediately from the definitions of:
* complementary projection
* complementary idempotent
where the constructions of the complementary projection and the complementary idempotent from $A$ are identical.
{{qed}}
Category:Linear Transformations on Hilbert Spaces
0uhdd105kmpbue9fpexqw9rbia9wmbm
Theorem: Möbius Transformations form Group under Composition

Let $G$ be the set of Möbius transformations.
Let $\circ$ denote the composition of mappings.
Then $\struct {G, \circ}$ is a group.

Proof:
Taking the group axioms in turn:
Theorem: Distance between Excenters 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 $I_b$ and $I_c$ be the excenters of $\triangle ABC$ {{WRT}} $b$ and $c$ respectively.
Let $R$ be the circumradius of $\triangle ABC$.
Then:
:$I_b I_c = 4 R \cos \dfrac A 2$

Proof:
:560px
From Triangle is Orthic Triangle of Triangle formed from Excenters, we establish that $\triangle ABC$ is the orthic triangle of $\triangle I_a I_b I_c$.
Hence $I_b B$ is an altitude of $\triangle I_a I_b I_c$.
Thus $\angle I_b B I_a$ is a right angle.
From Altitudes of Triangle Bisect Angles of Orthic Triangle:
:$\angle CBI = \dfrac B 2$
So:
:$\angle I_a B C = 90 \degrees - \dfrac B 2$
By a similar argument, {{mutatis}}:
:$\angle I_a C B = 90 \degrees - \dfrac C 2$
Hence:
{{begin-eqn}}
{{eqn | q = 
      | l = \angle B I_a C
      | r = 180 \degrees - \paren {\angle I_a B C + \angle I_a C B}
      | c = Sum of Angles of Triangle equals Two Right Angles
}}
{{eqn | r = 180 \degrees - \paren {\paren {90 \degrees - \dfrac B 2} + \paren {90 \degrees - \dfrac C 2} }
      | c = 
}}
{{eqn | r = \dfrac {B + C} 2
      | c = 
}}
{{eqn | r = \dfrac {180 \degrees - A} 2
      | c = Sum of Angles of Triangle equals Two Right Angles
}}
{{eqn | r = 90 \degrees - \dfrac A 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = BC
      | r = I_b I_c \map \cos {90 \degrees - \dfrac A 2}
      | c = Sides of Orthic Triangle of Acute Triangle
}}
{{eqn | ll= \leadsto
      | l = I_b I_c
      | r = \dfrac a {\sin \frac A 2}
      | c = Cosine of Complement equals Sine
}}
{{eqn | ll= \leadsto
      | r = \dfrac {2 R \sin A} {\sin \frac A 2}
      | c = Law of Sines
}}
{{eqn | ll= \leadsto
      | r = \dfrac {2 R \cdot 2 \sin \frac A 2 \cos \frac A 2} {\sin \frac A 2}
      | c = Double Angle Formula for Sine
}}
{{eqn | ll= \leadsto
      | r = 4 R \cos \frac A 2
      | c = Double Angle Formula for Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Distance between Incenter and Excenter 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 $I$ be the incenter of $\triangle ABC$.
Let $I_a$ be the excenter of $\triangle ABC$ {{WRT}} $a$.
Let $R$ be the circumradius of $\triangle ABC$.
Then:
:$I I_a = 4 R \sin \dfrac A 2$

Proof:
:560px
From Triangle is Orthic Triangle of Triangle formed from Excenters, we establish that $\triangle ABC$ is the orthic triangle of $\triangle I_a I_b I_c$.
By the Nine Point Circle Theorem, the Feuerbach circle of $\triangle I_a I_b I_c$ passes through each of $A$, $B$ and $C$.
Therefore the Feuerbach circle of $\triangle I_a I_b I_c$ is the circumcircle of $\triangle ABC$.
Hence the radius of the Feuerbach circle is $R$.
From Radius of Circumcircle is Twice Radius of Feuerbach Circle, the radius of the circumcircle of $\triangle I_a I_b I_c$ is $2 R$.
Hence:
{{begin-eqn}}
{{eqn | q = 
      | l = I I_a
      | r = 2 \paren {2 R} \map \cos {90 \degrees - \dfrac A 2}
      | c = Distance from Vertex of Triangle to Orthocenter
}}
{{eqn | ll= \leadsto
      | r = 4 R \sin \frac A 2
      | c = Cosine of Complement equals Sine
}}
{{end-eqn}}
{{WIP|Extract a lemma from Distance between Excenters of Triangle in Terms of Circumradius that gives $\angle B I_a C {{=}} 90 \degrees - \dfrac A 2$}}
{{qed}}
Theorem: Condition for Linear Dependence of Linear Functionals in terms of Kernel

Let $V$ be a vector space over a field $\GF$.
Let $f, f_1, \ldots, f_n: V \to \GF$ be linear functionals.
Suppose that:
:$\ds \bigcap_{i \mathop = 1}^n \ker f_i \subseteq \ker f$
where $\ker f$ denotes the kernel of $f$.
Then there exist $\alpha_1, \ldots, \alpha_n \in \GF$ such that:
:$\ds \forall v \in V: \map f v = \sum_{i \mathop = 1}^n \alpha_i \map {f_i} v$
That is: 
:$f \in \span \set {f_1, \ldots, f_n}$

Proof:
For $i = 1, \ldots, n$, let $w_i$ be such that:
:$w_i \not\in \ker f_i$
:$w_i \in \ker f_j, j \ne i$
Suppose first that the $w_i$ all exist.
Let $v_i = \dfrac 1 {\map {f_i} {w_i} } w_i$.
Then since $f_i$ is linear:
:$\map {f_i} {v_i} = 1$
Furthermore for $j \ne i$, $\map {f_j} {v_i} = 0$.
Now let $v \in V$ be arbitrary, and define:
:$\ds w = v - \sum_{i \mathop = 1}^n \map {f_i} v v_i$
Then:
{{begin-eqn}}
{{eqn|l = \map {f_j} w
     |r = \map {f_j} v - \sum_{i \mathop = 1}^n \map {f_i} v \map {f_j} {v_i}
}}
{{eqn|r = \map {f_j} v - \map {f_j} v
     |c = $\map {f_i} {v_i} {{=}} 1, \map {f_j} {v_i} {{=}} 0$
}}
{{eqn|r = 0
}}
{{end-eqn}}
Since $j$ was arbitrary, it follows from the premise on $f$ that:
:$\map f w = 0$
That is to say:
:$\ds 0 = \map f v - \sum_{i \mathop = 1}^n \map {f_i} v \map f {v_i}$
Setting $\alpha_i = \map f {v_i}$ we find:
:$\ds \map f v = \sum_{i \mathop = 1}^n \alpha_i \map {f_i} v$
{{qed|lemma}}
Now the case that such $w_i$ does not exist for a particular $i$.
Then:
:$\ds \bigcap_{i \mathop = 1}^n \ker f_i = \bigcap_{j \mathop \ne i} \ker f_j$
and $\set{ f_j: j \ne i}$ fulfils the condition of the result.
The result for $f_1, \ldots, f_n$ follows by setting $\alpha_i = 0$.
{{qed}}
Theorem: Condition for Linear Dependence of Linear Functionals in terms of Kernel

Let $V$ be a vector space over a field $\GF$.
Let $f, f_1, \ldots, f_n: V \to \GF$ be linear functionals.
Suppose that:
:$\ds \bigcap_{i \mathop = 1}^n \ker f_i \subseteq \ker f$
where $\ker f$ denotes the kernel of $f$.
Then there exist $\alpha_1, \ldots, \alpha_n \in \GF$ such that:
:$\ds \forall v \in V: \map f v = \sum_{i \mathop = 1}^n \alpha_i \map {f_i} v$
That is: 
:$f \in \span \set {f_1, \ldots, f_n}$

Proof:
Define $T : X \to {\GF}^n$ by: 
:$\map T x = \paren {\map {g_1} x, \map {g_2} x, \ldots, \map {g_n} x}$
for each $x \in X$.
We show that $T$ is linear. 
Let $x, y \in X$ and $\alpha, \beta \in \GF$. 
We have: 
{{begin-eqn}}
{{eqn	| l = \map T {\alpha x + \beta y}
		| r = \tuple {\map {g_1} {\alpha x + \beta y}, \map {g_2} {\alpha x + \beta y}, \ldots, \map {g_n} {\alpha x + \beta y} }
}}
{{eqn	| r = \tuple {\alpha \map {g_1} x + \beta \map {g_1} y, \alpha \map {g_2} x + \beta \map {g_2} y, \ldots, \alpha \map {g_n} x + \beta \map {g_n} y}
		| c = $g_i$ is linear
}}
{{eqn	| r = \alpha \tuple {\map {g_1} x, \ldots, \map {g_n} x} + \beta \tuple {\map {g_1} y, \ldots, \map {g_n} y}
}}
{{eqn	| r = \alpha T x + \beta T y
}}
{{end-eqn}}
so $T$ is linear.
Now, we have $\map T x = 0$ {{iff}} $\map {g_i} x = 0$ for each $x \in X$. 
That is, {{iff}}:
:$\ds x \in \bigcap_{i \mathop = 1}^n \ker g_i$
so that:
:$\ds \ker T = \bigcap_{i \mathop = 1}^n \ker g_i \subseteq \ker f$
Now, suppose that $x, y \in X$ have $T x = T y$.
Then by the linearity of $T$, we have: 
:$\map T {x - y} = 0$
so $x - y \subseteq \ker f$.
So $\map f {x - y} = 0$, and hence $\map f x = \map f y$, for these $x, y \in X$.
We can therefore define a map $\widetilde f : \Img T \to \GF$ by: 
:$\map {\widetilde f} {\map T x} = \map f x$ 
for each $x \in \Img T$.
From Image of Vector Subspace under Linear Transformation is Vector Subspace, $\Img T$ is a vector subspace of ${\GF}^n$.
Let $\set {e_1, \ldots, e_n}$ be the standard basis for ${\GF}^n$.
Let $\set {v_1, \ldots, v_k}$ be a basis of $\Img T$.
From Linearly Independent Set is Contained in some Basis, $\set {v_1, \ldots, v_k}$ is contained in some basis $\set {v_1, \ldots, v_n}$ of ${\GF}^n$. 
Define the mapping $h : {\GF}^n \to \GF$ by taking: 
:$\ds \map h {v_i} = \map {\widetilde f} {v_i}$ for $1 \le i \le k$
and:
:$\ds \map h {v_i} = 0$ for $k < i \le n$
and taking: 
:$\ds \map h {\sum_{i \mathop = 1}^n \alpha_i v_i} = \sum_{i \mathop = 1}^n \alpha_i \map h {v_i}$ 
for scalars $\alpha_1, \alpha_2, \ldots, \alpha_n \in \GF$.
By construction, $h$ is a linear functional.
We then have, for each $x \in X$: 
{{begin-eqn}}
{{eqn	| l = \map f x
		| r = \map {\widetilde f} {\map T x}
}}
{{eqn	| r = \map h {\map T x}
		| c = since $h$ and $\widetilde f$ coincide on $\Img T$
}}
{{eqn	| r = \map h {\sum_{i \mathop = 1}^n \map {g_i} x e_i}
}}
{{eqn	| r = \sum_{i \mathop = 1}^n \map {g_i} x \map h {e_i}
}}
{{end-eqn}}
with $\map h {e_i} \in \GF$.
So we have: 
:$f \in \span \set {g_1, \ldots, g_n}$
{{qed}}
Theorem: Open Neighborhoods of Point form Directed Ordering

Let $\struct{ S, \tau }$ be a topological space.
Let $x \in S$.
Let $\NN \subseteq \tau$ be the set of open neighborhoods of $x$.
Then $\supseteq$, the ordering of $\NN$ by reverse inclusion, is a directed ordering on $\NN$.

Proof:
By Subset Relation is Ordering and Dual Ordering is Ordering $\supseteq$ is an ordering on $\NN$.
To show that $\supseteq$ is directed, let $U, V \in \NN$.
Then $x \in U, V$, so that $x \in U \cap V$.
Hence $U \cap V \in \NN$ is an open neighborhood of $x$.
Moreover by Intersection is Subset:
:$U, V \supseteq U \cap V$
Hence $\supseteq$ is directed.
{{qed}}
Theorem: Finite Subsets form Directed Ordering

Let $I$ be a set.
Denote with $\FF$ the set of finite subsets of $I$.
Let $\subseteq$ be the subset relation on $\FF$.
Then $\subseteq$ is a directed ordering on $\FF$.

Proof:
From Subset Relation is Ordering, we know that $\subseteq$ is an ordering.
Now let $F, G \in \FF$.
From Set Union Preserves Subsets, conclude that $F \cup G \subseteq I$ as $F, G \subseteq I$.
From Union of Finite Sets is Finite, $F \cup G$ is a finite set.
Hence $F \cup G \in \FF$.
Furthermore, $F \subseteq F \cup G$ and $G \subseteq F \cup G$.
It follows that $\subseteq$ is a directed ordering.
{{qed}}
Theorem: Quotient Ring of Noetherian Ring is Noetherian

Let $A$ be a Noetherian ring.
Let $\mathfrak a \subseteq A$ be an ideal.
Let $A / \mathfrak a$ be the quotient ring of $A$ by $\mathfrak a$.
Then $A / \mathfrak a$ is a Noetherian ring.

Proof:
Observe that:
:$0 \longrightarrow \mathfrak a \longrightarrow A \longrightarrow A / \mathfrak a \longrightarrow 0$
is a short exact sequence of $A$-modules.
By Short Exact Sequence Condition of Noetherian Modules, $A / \mathfrak a$ is a Noetherian $A$-module.
As $A / \mathfrak a$ is an $A / \mathfrak a$-module, $A / \mathfrak a$ is also a Noetherian $A / \mathfrak a$-module.
{{explain|We know that $A / \mathfrak a$ is an $A$-module, but how do we know $A / \mathfrak a$ is an $A / \mathfrak a$-module?}}
By {{Defof|Noetherian Ring|index = 4}}, $A / \mathfrak a$ is a Noetherian ring.
{{qed}}
Category:Noetherian Rings
r4asilfwmjvm8uccp7wpd24391cop9i
Theorem: Absolute Value of Trigonometric Function

Let $\theta$ be an angle embedded in a Cartesian plane.
Let $\theta$ be such that the vertex of $\theta$ is located at the origin while one arm is coincident with the $x$-axis.
Let $\phi$ be the acute angle made by the other arm with the $x$-axis.
Let $f: \R \to \R$ be a trigonometric function.
Then $\size {\map f \theta}$ is equal to $\map f \phi$.
That is, a trigonometric function of an angle can be calculated by working out its quadrant to determine its sign, then using the equivalent value of what it is between $0$ and $90 \degrees$ to get its value.
{{improve}}

Proof:
One of the following applies:
:$\theta = \phi$
:$\theta = -\paren {\phi + \pi}$
:$\theta = \phi + \pi$
:$\theta = -\phi$
depending on the quadrant.
{{explain|prove the above}}
Substituting $\theta$ in $\size {\map f \theta}$ with any of the above expressions, we simplify by using
{{begin-eqn}}
{{eqn | l = \size {\map f {\alpha + \pi} }
      | r = \size {\map f \alpha}
      | c = 
}}
{{eqn | l = \size {\map f {-\alpha} }
      | r = \size {\map f \alpha}
      | c = 
}}
{{eqn | l = \size {\map f \phi}
      | r = \map f \phi
      | c = 
}}
{{end-eqn}}
to obtain:
:$\size {\map f \theta} = \map f \phi$
{{qed}}
Theorem: Tangent of Angle minus Three Right Angles

:$\map \tan {x - \dfrac {3 \pi} 2} = \cot x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \tan {x - \dfrac {3 \pi} 2}
      | r = -\map \tan {x - \dfrac {\pi} 2}
      | c = as $\map \tan {x - \dfrac {\pi} 2}$ is in the opposite quadrant to $\map \tan {x - \dfrac {3 \pi} 2}$
}}
{{eqn | r = \cot \theta
      | c = Tangent of Complement equals Cotangent
}}
{{end-eqn}}
{{qed}}
Theorem: Reciprocal of One Minus Cosine plus Reciprocal of One Plus Cosine

:$\dfrac 1 {1 - \cos x} + \dfrac 1 {1 + \cos x} = 2 \cosec^2 x$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac 1 {1 - \cos x} + \dfrac 1 {1 + \cos x}
      | r = \dfrac {\paren {1 + \cos x} + \paren {1 - \cos x} } {\paren {1 - \cos x} \paren {1 + \cos x} }
      | c = common denominator
}}
{{eqn | r = \dfrac 2 {1 - \cos^2 x}
      | c = Difference of Two Squares and simplification
}}
{{eqn | r = \dfrac 2 {\sin^2 x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = 2 \cosec^2 x
      | c = Cosecant is Reciprocal of Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Product of One Plus Cotangent with One Plus Tangent

:$\paren {1 + \cot x} \paren {1 + \tan x} = 2 + \csc x \sec x$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {1 + \cot x} \paren {1 + \tan x}
      | r = 1 + \cot x + \tan x + \cot x \tan x
      | c = multiplying out
}}
{{eqn | r = 1 + \cot x + \tan x + \dfrac 1 {\tan x} \tan x
      | c = Cotangent is Reciprocal of Tangent
}}
{{eqn | r = 2 + \cot x + \tan x
      | c = simplifying
}}
{{eqn | r = 2 + \csc x \sec x
      | c = Sum of Tangent and Cotangent
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine over Cosine of Complement plus Sine over Sine of Complement

:$\dfrac {\cos x} {\map \cos {90 \degrees - x} } + \dfrac {\sin x} {\map \sin {90 \degrees - x} } = \csc x \sec x$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {\cos x} {\map \cos {90 \degrees - x} } + \dfrac {\sin x} {\map \sin {90 \degrees - x} }
      | r = \dfrac {\cos x} {\sin x} + \dfrac {\sin x} {\cos x}
      | c = Cosine of Complement equals Sine, Sine of Complement equals Cosine
}}
{{eqn | r = \cot x + \tan x
      | c = Cotangent is Cosine divided by Sine, Tangent is Sine divided by Cosine
}}
{{eqn | r = \csc x \sec x
      | c = Sum of Tangent and Cotangent
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Fourth Powers of Sine and Cosine

:$\cos^4 x + \sin^4 x = 1 - 2 \cos^2 x \sin^2 x$

Proof:
{{begin-eqn}}
{{eqn | l = \cos^4 x + \sin^4 x
      | r = \cos^2 x \paren {1 - \sin^2 x} + \sin^2 x \paren {1 - \cos^2 x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \cos^2 x + \sin^2 x - 2 \cos^2 x \sin^2 x
      | c = simplification
}}
{{eqn | r = 1 - 2 \cos^2 x \sin^2 x
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Fourth Powers of Sine and Cosine

:$\cos^4 x + \sin^4 x = 1 - 2 \cos^2 x \sin^2 x$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\cos^2 x + \sin^2 x}^2
      | r = 1
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll = \leadsto
      | l = \cos^4 x + 2 \cos^2 x \sin^2 x + \sin^4 x
      | r = 1
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \cos^4 x + \sin^4 x
      | r = 1 - 2 \cos^2 x \sin^2 x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Cubes of Sine and Cosine

:$\cos^3 x + \sin^3 x = \paren {\cos x + \sin x} \paren {1 - \cos x \sin x}$

Proof:
{{begin-eqn}}
{{eqn | l = \cos^3 x + \sin^3 x
      | r = \cos x \paren {1 - \sin^2 x} + \sin x \paren {1 - \cos^2 x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \cos x + \sin x - \cos x \sin x \paren {\cos x + \sin x}
      | c = simplification
}}
{{eqn | r = \paren {\cos x + \sin x} \paren {1 - \cos x \sin x}
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Spectrum of Self-Adjoint Bounded Linear Operator is Real

Let $\struct {\HH, \innerprod \cdot \cdot}$ be a Hilbert space over $\C$. 
Let $T : \HH \to \HH$ be a bounded self-adjoint operator.
Let $\map \sigma T$ be the spectrum of $T$.
Then:
:$\map \sigma T \subseteq \R$

Proof:
This follows from:
:Spectrum of Self-Adjoint Densely-Defined Linear Operator is Real and Closed
:Spectrum of Bounded Linear Operator equal to Spectrum as Densely-Defined Linear Operator
{{qed}}
Theorem: Spectrum of Self-Adjoint Bounded Linear Operator is Real

Let $\struct {\HH, \innerprod \cdot \cdot}$ be a Hilbert space over $\C$. 
Let $T : \HH \to \HH$ be a bounded self-adjoint operator.
Let $\map \sigma T$ be the spectrum of $T$.
Then:
:$\map \sigma T \subseteq \R$

Proof:
Let $\lambda := a + i b \in \C \setminus \R$.
Note that $b \ne 0$.
For all $\phi \in \HH$:
{{begin-eqn}}
{{eqn | l = \norm {\paren {T - \lambda I} \phi}^2
      | r = \norm {\paren {T - a I} \phi}^2 + b^2 \norm {\phi}^2
      | c = as $\Re \innerprod {\paren {T - a I} \phi} {- i b \phi} = 0$
}}
{{eqn | o = \ge
      | r = b^2 \norm {\phi}^2
      | n = 1
}}
{{end-eqn}}
In view of $(1)$, both $T - \lambda I$ and $T - \overline \lambda I$ are injective.
Moreover:
{{begin-eqn}}
{{eqn | l = \paren {\Img {T - \lambda I} }^\perp
      | r = \paren {\Img { \paren {T - \overline \lambda I}^\ast } }^\perp
      | c = as $T - \lambda I = \paren {T - \overline \lambda I}^\ast$
}}
{{eqn | r = \ker \paren {T - \overline \lambda I}
      | c = Kernel of Linear Transformation is Orthocomplement of Image of Adjoint
}}
{{eqn | r = \set 0
      | c = as $T - \overline \lambda I$ is injective
}}
{{end-eqn}}
By Linear Subspace Dense iff Zero Orthocomplement, $\Img {T - \lambda I}$ is dense in $\HH$.
Let $\phi \in \HH$.
Then there exists an $\sequence {\psi _n} \subseteq \HH$ such that:
:$\paren {T - \lambda I} \psi_n \to \phi$
By $(1)$ there exists a $\psi \in \HH$ such that:
:$\psi_n \to \psi$
and:
:$\paren {T - \lambda I} \psi = \phi$
Thus $T - \lambda I$ is surjective.
In addition, by $(1)$ we have:
:$\norm \psi \le \size b^{-1} \norm \phi$
Therefore $T - \lambda I$ is invertible such that:
:$\norm {\paren {T - \lambda I}^{-1} } \le \size b^{-1}$
That is, $\lambda \not \in \map \sigma T$.
{{qed}}
Theorem: Convergent Sequences form Invariant Subspace of Bounded Sequences wrt Cesàro Summation Operator

Let $\ell^\infty$ be the space of bounded sequences.
Let $c$ be the space of convergent sequences.
Let $A : \ell^\infty \to \ell^\infty$ be the Cesàro summation operator.
Then $c$ is an invariant subspace of $\ell^\infty$ {{WRT}} $A$.

Proof:
Let $\sequence {x_n}_{n \mathop \in \N} \in c$ be a sequence.
By definition, $\sequence {x_n}_{n \mathop \in \N}$ converges.
Let $\ds L = \lim_{n \mathop \to \infty} x_n$ be the limit of $\sequence {x_n}_{n \mathop \in \N}$.
Then:
:$\forall \epsilon \in \R_{> 0} : \exists N_1 \in \N : \forall n \in \N : n > N_1 \implies \size {x_n - L} < \epsilon$
Furthermore:
:$\exists M \in \R_{> 0} : \forall n \in \N : \size {x_n} < M$
Theorem: First Fundamental Group of 1-Sphere

Let $\mathbb S^1$ be the $1$-sphere.
Let $\struct {\map {\pi _1} {\mathbb S^1}, \ast}$ be the first fundamental group of $\mathbb S^1$.
Let $\struct {\Z, +}$ be the additive group of integers.
Then $\struct {\map {\pi _1} {\mathbb S^1}, \ast}$ is isomorphic to $\struct {\Z, +}$.

Proof:
We are given that $\struct {\map {\pi _1} {\mathbb S^1}, \ast}$ is the first fundamental group of $\mathbb S^1$.
Let $x_0 \in \mathbb S^1$.
Let $\struct{\mathbb S^1, x_0}$ be the pointed topological space for $\mathbb S^1$.
Since Fundamental Group is Independent of Base Point for Path-Connected Space, what to be proved is:
:$\struct {\map {\pi _1} {\mathbb S^1, x_0}, \ast} \cong \struct {\Z, +}$ 
where the map:
:$\ast : \map {\pi_1} {\mathbb S^1, x_0} \times \map {\pi_1} {\mathbb S^1, x_0} \to \map {\pi_n} {\mathbb S^1, x_0}$ 
denotes the concatenation of homotopy classes of paths.
{{ProofWanted}}
Hence $\struct {\map {\pi _1} {\mathbb S^1}, \ast}$ is isomorphic to $\struct {\Z, +}$.
Category:Homotopy Theory
llgbwqyrqv8ii7rxp89ln6zfs6n1p5a
Theorem: Sum of Sides of Triangle in terms of Circumradius and Half Angle Cosines

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:
:$a + b + c = 8 R \cos \dfrac A 2 \cos \dfrac B 2 \cos \dfrac C 2$
where $R$ denotes the circumradius of $\triangle ABC$.

Proof:
From Law of Sines:
:$\dfrac a {\sin A} = \dfrac b {\sin B} = \dfrac c {\sin C} = 2 R$
Hence:
{{begin-eqn}}
{{eqn | l = a
      | r = 2 R \sin A
}}
{{eqn | l = b
      | r = 2 R \sin B
}}
{{eqn | l = c
      | r = 2 R \sin C
}}
{{eqn | ll= \leadsto
      | l = a + b + c
      | r = 2 R \paren {\sin A + \sin B + \sin C}
      | c = 
}}
{{eqn | r = 2 R \paren {4 \cos \dfrac A 2 \cos \dfrac B 2 \cos \dfrac C 2}
      | c = Sum of Sines of Angles in Triangle
}}
{{eqn | r = 8 R \cos \dfrac A 2 \cos \dfrac B 2 \cos \dfrac C 2
      | c = 
}}
{{end-eqn}}
{{qed}}