avewright/proofwiki-math huggingface dataset:
Theorem: Exponential Form of Complex Conjugate

Let $z := r e^{i \theta} \in \C$ be a complex number expressed in exponential form.
Then:
:$\overline z = r e^{-i \theta}$
where $\overline z$ denotes the complex conjugate of $z$.

Proof:
{{begin-eqn}}
{{eqn | l = z
      | r = r e^{i \theta}
      | c = 
}}
{{eqn | r = r \paren {\cos \theta + i \sin \theta}
      | c = Euler's Formula
}}
{{eqn | ll= \leadsto
      | l = \overline z
      | r = r \paren {\cos \theta - i \sin \theta}
      | c = Polar Form of Complex Conjugate
}}
{{eqn | r = r e^{-i \theta}
      | c = {{Corollary|Euler's Formula}}
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Dot Product in Exponential Form

Let $z_1 := r_1 e^{i \theta_1}, z_2 := r_2 e^{i \theta_2} \in \C$ be complex numbers expressed in exponential form.
Then:
:$z_1 \circ z_2 = r_1 r_2 \, \map \cos {\theta_2 - \theta_1}$
where $z_1 \circ z_2$ denotes the dot product of $z_1$ and $z_2$.

Proof:
{{begin-eqn}}
{{eqn | l = z_1 \circ z_2
      | r = \map \Re {\overline {z_1} z_2}
      | c = {{Defof|Dot Product|subdef = Complex|index = 3}}
}}
{{eqn | r = \map \Re {r_1 e^{-i \theta_1} r_2 e^{i \theta_2} }
      | c = Exponential Form of Complex Conjugate
}}
{{eqn | r = \map \Re {r_1 r_2 e^{i \paren {\theta_2 - \theta_1} } }
      | c = Product of Complex Numbers in Exponential Form
}}
{{eqn | r = \map \Re {r_1 r_2 \paren {\map \cos {\theta_2 - \theta_1} + i \, \map \sin {\theta_2 - \theta_1} } }
      | c = {{Defof|Polar Form of Complex Number}}
}}
{{eqn | r = r_1 r_2 \map \cos {\theta_2 - \theta_1}
      | c = {{Defof|Real Part}}
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Cross Product in Exponential Form

Let $z_1 := r_1 e^{i \theta_1}, z_2 := r_2 e^{i \theta_2} \in \C$ be complex numbers expressed in exponential form.
Then:
:$z_1 \times z_2 = r_1 r_2 \map \sin {\theta_2 - \theta_1}$
where $z_1 \times z_2$ denotes the dot product of $z_1$ and $z_2$.

Proof:
{{begin-eqn}}
{{eqn | l = z_1 \times z_2
      | r = \map \Im {\overline {z_1} z_2}
      | c = {{Defof|Vector Cross Product|subdef = Complex|index = 3|Complex Cross Product}}
}}
{{eqn | r = \map \Im {r_1 e^{-i \theta_1} r_2 e^{i \theta_2} }
      | c = Exponential Form of Complex Conjugate
}}
{{eqn | r = \map \Im {r_1 r_2 e^{i \paren {\theta_2 - \theta_1} } }
      | c = Product of Complex Numbers in Exponential Form
}}
{{eqn | r = \map \Im {r_1 r_2 \paren {\map \cos {\theta_2 - \theta_1} + i \map \sin {\theta_2 - \theta_1} } }
      | c = {{Defof|Polar Form of Complex Number}}
}}
{{eqn | r = r_1 r_2 \map \sin {\theta_2 - \theta_1}
      | c = {{Defof|Imaginary Part}}
}}
{{end-eqn}}
{{qed}}
Theorem: Dot Product Distributes over Addition

:$\paren {\mathbf u + \mathbf v} \cdot \mathbf w = \mathbf u \cdot \mathbf w + \mathbf v \cdot \mathbf w$

Proof:
{{begin-eqn}}
{{eqn | l = \left({\mathbf u + \mathbf v}\right) \cdot \mathbf w
      | r = \sum_{i \mathop = 1}^n \left({u_i + v_i}\right) w_i
      | c = {{Defof|Vector Sum}} and {{Defof|Dot Product}}
}}
{{eqn | r = \sum_{i \mathop = 1}^n \left({u_i w_i + v_i w_i}\right)
      | c = Real Multiplication Distributes over Real Addition
}}
{{eqn | r = \sum_{i \mathop = 1}^n u_i w_i + \sum_{i \mathop = 1}^n v_i w_i
      | c =
}}
{{eqn | r = \mathbf u \cdot \mathbf w + \mathbf v \cdot \mathbf w
      | c = {{Defof|Dot Product}}
}}
{{end-eqn}}
{{qed}}
Theorem: Dot Product Distributes over Addition

:$\paren {\mathbf u + \mathbf v} \cdot \mathbf w = \mathbf u \cdot \mathbf w + \mathbf v \cdot \mathbf w$

Proof:
Let the vectors $\mathbf u$, $\mathbf v$ and $\mathbf w$ be embedded in a Cartesian $3$-space.
It is noted that $\mathbf u$, $\mathbf v$ and $\mathbf w$ are not necessarily coplanar.
:520px
Let instances of $\mathbf u$ and $\mathbf w$ be selected so their initial points are at some point $O$.
Let an instance of $\mathbf v$ be selected so its initial point is positioned at the terminal point $U$ of $\mathbf u$.
Let the terminal point $\mathbf v$ be $V$.
Let $UA$ be dropped perpendicular to $\mathbf w$.
Let $VB$ be dropped perpendicular to $\mathbf w$.
Let another instance of $\mathbf w$ be selected so that its initial point is at $U$.
Let $VC$ be dropped perpendicular to this second instance of $\mathbf w$.
Let $CB$ be dropped from $C$ to the first instance of $\mathbf w$.
We have that:
:$UA \parallel CB$
and:
:$UC \parallel AB$
Thus $\Box ABCU$ is a parallelogram.
Hence:
:$AB = UC$
Then we have that:
{{begin-eqn}}
{{eqn | l = OA
      | r = OU \cos \angle \mathbf u, \mathbf w
      | c = 
}}
{{eqn | r = \norm {\mathbf u} \cos \angle \mathbf u, \mathbf w
      | c = 
}}
{{eqn | l = AB
      | r = UV \cos \angle \mathbf v, \mathbf w
      | c = 
}}
{{eqn | r = \norm {\mathbf v} \cos \angle \mathbf v, \mathbf w
      | c = 
}}
{{eqn | l = OB
      | r = OV \cos \angle \paren {\mathbf u + \mathbf v}, \mathbf w
      | c = 
}}
{{eqn | r = \norm {\paren {\mathbf u + \mathbf v} } \cos \angle \paren {\mathbf u + \mathbf v}, \mathbf w
      | c = 
}}
{{eqn | r = \norm {\mathbf u} \cos \angle \mathbf u, \mathbf w + \norm {\mathbf v} \cos \angle \mathbf v, \mathbf w
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \norm {\paren {\mathbf u + \mathbf v} } \norm {\mathbf w} \cos \angle \paren {\mathbf u + \mathbf v}, \mathbf w
      | r = \norm {\mathbf u} \norm {\mathbf w} \cos \angle \mathbf u, \mathbf w + \norm {\mathbf v} \norm {\mathbf w} \cos \angle \mathbf v, \mathbf w
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\mathbf u + \mathbf v} \cdot \mathbf w
      | r = \mathbf u \cdot \mathbf w + \mathbf v \cdot \mathbf w
      | c = {{Defof|Dot Product|subdef = Real Euclidean Space}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Dot Product Distributes over Addition

:$\paren {\mathbf u + \mathbf v} \cdot \mathbf w = \mathbf u \cdot \mathbf w + \mathbf v \cdot \mathbf w$

Proof:
From Dot Product Operator is Bilinear:
:$\paren {c \mathbf u + \mathbf v} \cdot \mathbf w = c \paren {\mathbf u \cdot \mathbf w} + \paren {\mathbf v \cdot \mathbf w}$
Setting $c = 1$ yields the result.
{{qed}}
Theorem: Dot Product Operator is Bilinear

:$\paren {c \mathbf u + \mathbf v} \cdot \mathbf w = c \paren {\mathbf u \cdot \mathbf w} + \paren {\mathbf v \cdot \mathbf w}$
:$\mathbf u \cdot \paren {c \mathbf v + \mathbf w} = c \paren {\mathbf u \cdot \mathbf v} + \paren {\mathbf u \cdot \mathbf w}$

Proof:
Let $V$ have $n$ dimensions.
Theorem: Dot Product Associates with Scalar Multiplication

:$\paren {c \mathbf u} \cdot \mathbf v = c \paren {\mathbf u \cdot \mathbf v}$

Proof:
{{begin-eqn}}
{{eqn | l = \left({c \mathbf u}\right) \cdot \mathbf v
      | r = \sum_{i \mathop = 1}^n \left({c u_i}\right) v_i
      | c = {{Defof|Dot Product}}
}}
{{eqn | r = \sum_{i \mathop = 1}^n c \left({ u_i v_i }\right)
      | c = Real Multiplication is Associative
}}
{{eqn | r = c \sum_{i \mathop = 1}^n u_i v_i
      | c = Real Multiplication Distributes over Real Addition
}}
{{eqn | r = c \left({\mathbf u \cdot \mathbf v}\right)
      | c = {{Defof|Dot Product}}
}}
{{end-eqn}}
{{qed}}
Theorem: Dot Product Associates with Scalar Multiplication

:$\paren {c \mathbf u} \cdot \mathbf v = c \paren {\mathbf u \cdot \mathbf v}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {c \mathbf u} \cdot \mathbf v
      | r = \norm {c \mathbf u} \norm {\mathbf v} \cos \angle c \mathbf u, \mathbf v
      | c = {{Defof|Dot Product}}
}}
{{eqn | r = \sqrt {\sum_{i \mathop = 1}^n \paren {c u_i}^2} \norm {\mathbf v} \cos \angle c \mathbf u, \mathbf v
      | c = {{Defof|Vector Length|Vector Length in $\R^n$}}
}}
{{eqn | r = \sqrt {c^2 \sum_{i \mathop = 1}^n u_i^2} \norm {\mathbf v} \cos \angle \mathbf u, \mathbf v
      | c = $c \mathbf u$ and $\mathbf u$ are in the same direction
}}
{{eqn | r = c \sqrt {\sum_{i \mathop = 1}^n u_i^2} \norm {\mathbf v} \cos \angle \mathbf u, \mathbf v
      | c =
}}
{{eqn | r = c \norm {\mathbf u} \norm {\mathbf v} \cos \angle \mathbf u, \mathbf v
      | c = {{Defof|Vector Length|Vector Length in $\R^n$}}
}}
{{eqn | r = c \paren {\mathbf u \cdot \mathbf v}
      | c = {{Defof|Dot Product}}
}}
{{end-eqn}}
{{qed}}
Theorem: Dot Product Associates with Scalar Multiplication

:$\paren {c \mathbf u} \cdot \mathbf v = c \paren {\mathbf u \cdot \mathbf v}$

Proof:
From Dot Product Operator is Bilinear:
:$\left({c \mathbf u + \mathbf v}\right) \cdot \mathbf w = c \left({\mathbf u \cdot \mathbf w}\right) + \left({\mathbf v \cdot \mathbf w}\right)$
Setting $\mathbf v = 0$ and renaming $\mathbf w$ yields the result.
{{qed}}
Theorem: Complex Cross Product Distributes over Addition

Let $z_1, z_2, z_3 \in \C$ be complex numbers.
Then:
:$z_1 \times \paren {z_2 + z_3} = z_1 \times z_2 + z_1 \times z_3$
where $\times$ denotes cross product.

Proof:
Let:
:$z_1 = x_1 + i y_1$
:$z_2 = x_2 + i y_2$
:$z_3 = x_3 + i y_3$
Then:
{{begin-eqn}}
{{eqn | l = z_1 \times \paren {z_2 + z_3}
      | r = \paren {x_1 + i y_1} \times \paren {\paren {x_2 + i y_2} + \paren {x_3 + i y_3} }
      | c = 
}}
{{eqn | r = \paren {x_1 + i y_1} \times \paren {\paren {x_2 + x_3} + i \paren {y_2 + y_3} }
      | c = {{Defof|Complex Addition}}
}}
{{eqn | r = x_1 \left({y_2 + y_3}\right) - y_1 \left({x_2 + x_3}\right)
      | c = {{Defof|Vector Cross Product|subdef = Complex|index = 1|Complex Cross Product}}
}}
{{eqn | r = x_1 y_2 + x_1 y_3 - y_1 x_2 - y_1 x_3
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = x_1 y_2 - y_1 x_2 + x_1 y_3 - y_1 x_3
      | c = Real Addition is Commutative
}}
{{eqn | r = z_1 \times z_2 + z_1 \times z_3
      | c = {{Defof|Vector Cross Product|subdef = Complex|index = 1|Complex Cross Product}}
}}
{{end-eqn}}
{{qed}}
Theorem: Complement of Closed Set in Complex Plane is Open

Let $S \subseteq \C$ be a closed subset of the complex plane $\C$.
Then the complement of $S$ in $\C$ is open.

Proof:
{{begin-eqn}}
{{eqn | o =
      | c = $S$ is closed
}}
{{eqn | o = \leadsto
      | c = $\forall z \in \C: z$ is a limit point of $S \implies z \in S$
      | cc= {{Defof|Closed Set (Complex Analysis)|Closed Set}} 
}}
{{eqn | o = \leadsto
      | c = $\forall z \in \C: z \notin S \implies z$ is not a limit point of $S$
      | cc= Rule of Transposition
}}
{{eqn | o = \leadsto
      | c = $\forall z \in \C \setminus S \implies z$ is not a limit point of $S$
      | cc= {{Defof|Relative Complement}}
}}
{{eqn | o = \leadsto
      | c = $\forall z \in \C \setminus S:$ there exists a deleted $\epsilon$-neighborhood $\map {N_\epsilon} z \setminus \set z$ of $z$ entirely in $S$
      | cc= {{Defof|Limit Point (Complex Analysis)|Limit Point}}
}}
{{eqn | o = \leadsto
      | c = $\C \setminus S$ is open in $\C$
      | cc= {{Defof|Open Set (Complex Analysis)|Open Set}}
}}
{{end-eqn}}
{{qed}}
Theorem: Complement of Open Set in Complex Plane is Closed

Let $S \subseteq \C$ be an open subset of the complex plane $\C$.
Then the complement of $S$ in $\C$ is closed.

Proof:
{{begin-eqn}}
{{eqn | o =
      | c = $S$ is open in $\C$
      | cc=
}}
{{eqn | o = \leadsto
      | c = $\forall z \in S$: there exists a deleted $\epsilon$-neighborhood $\map {N_\epsilon} z \setminus \set z$ of $z$ entirely in $S$
      | cc= {{Defof|Open Set (Complex Analysis)|Open Set}}
}}
{{eqn | o = \leadsto
      | c = $\forall z \in \C: z \in S \implies z$ is not a limit point of $S$
      | cc= {{Defof|Limit Point (Complex Analysis)|Limit Point}}
}}
{{eqn | o = \leadsto
      | c = $\forall z \in \C: z$ is a limit point of $S \implies z \notin S$
      | cc= Rule of Transposition
}}
{{eqn | o = \leadsto
      | c = $\forall z \in \C: z$ is a limit point of $S \implies z \in \C \setminus S$
      | cc= {{Defof|Relative Complement}}
}}
{{eqn | o = \leadsto
      | c = $\C \setminus S$ is closed in $\C$
      | cc= {{Defof|Closed Set (Complex Analysis)|Closed Set}}
}}
{{end-eqn}}
{{qed}}
Theorem: Finite Union of Open Sets in Complex Plane is Open

Let $S_1, S_2, \ldots, S_n$ be open sets of $\C$.
Then $\ds \bigcup_{k \mathop = 1}^n S_k$ is an open set of $\C$.

Proof:
Let $\ds z \in \bigcup_{k \mathop = 1}^n S_k$.
Then by definition of finite union:
:$\exists k \in \set {1, 2, \ldots, n}: z \in S_k$
By definition of open set:
:$\exists \epsilon \in \R_{>0}: \map {N_\epsilon} z \subseteq S_k$
where $\map {N_\epsilon} z$ is the $\epsilon$-neighborhood of $z$ for $\epsilon$.
By Set is Subset of Union:
:$S_k \subseteq S$
Thus by Subset Relation is Transitive:
:$\map {N_\epsilon} z \subseteq S$
As $z$ is any arbitrary element of $S$, it follows that $S$ is an open set of $\C$ by definition.
{{qed}}
Theorem: Limit Point of Set in Complex Plane not Element is Boundary Point

Let $S \subseteq \C$ be a subset of the complex plane.
Let $z \in \C$ be a limit point of $S$ such that $z \notin S$.
Then $z$ is a boundary point of $S$.

Proof:
Let $z \in \C$ be a limit point of $S$ such that $z \notin S$.
Suppose $z$ is not a boundary point of $S$.
Then there exists an $\epsilon$-neighborhood $\map {N_\epsilon} z$ of $z$ such that either:
:$(1): \quad$ All elements of $\map {N_\epsilon} z$ are in $S$
or
:$(2): \quad$ All elements of $\map {N_\epsilon} z$ are not in $S$.
If $(1)$, then $z \in S$ which is a contradicts $z \notin S$.
If $(2)$, then $z$ is not a limit point of $S$, which also contradicts the conditions on $z$.
{{qed}}
Theorem: Condition for Quartic with Real Coefficients to have Wholly Imaginary Root

Let $Q$ be the quartic equation:
:$(1): \quad z^4 + a_1 z^3 + a_2 z^2 + a_3 z + a_4 = 0$
such that all of $a_1, a_2, a_3, a_4$ are real numbers.
Then $Q$ has a root which is wholly imaginary {{iff}}:
:$\text {(a)}: \quad a_3^2 + a_1^2 a_4 = a_1 a_2 a_3$
:$\text {(b)}: \quad a_1 a_3 > 0$

Proof:
=== Necessary Condition ===
We have:
{{begin-eqn}}
{{eqn | l = a_3^2 + a_1^2 a_4
      | r = a_1 a_2 a_3
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a_4
      | r = \frac {a_3} {a_1} \paren {a_2 - \frac {a_3} {a_1} }
      | c = 
}}
{{end-eqn}}
This leads to the factorisation of $(1)$:
{{begin-eqn}}
{{eqn | l = z^4 + a_1 z^3 + a_2 z^2 + a_3 z + a_4
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {z^2 + \frac {a_3} {a_1} } \paren {z^2 + a_1 z + \paren {a_2 - \frac {a_3} {a_1} } }
      | r = 0
      | c = 
}}
{{end-eqn}}
Two solutions to this are found from:
{{begin-eqn}}
{{eqn | l = z^2 + \frac {a_3} {a_1}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z^2
      | r = -\frac {a_3} {a_1}
      | c = 
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = z
      | r = \pm \sqrt {-\frac {a_3} {a_1} }
      | c =
}}
{{end-eqn}}
The other two solutions are found by solving:
{{begin-eqn}}
{{eqn | l = z^2 + a_1 z + \paren {a_2 - \frac {a_3} {a_1} }
      | r = 0
      | c = 
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = z
      | r = -\frac {a_1} 2 \pm \frac {\sqrt {a_1^2 - 4 \paren {a_2 - a_3 / a_1} } } 2
      | c = Quadratic Formula
}}
{{end-eqn}}
As $a_1 \ne 0$ it follows that $(3)$ always has a real part.
So only the $(2)$ can produce roots which are wholly imaginary, and that can happen only when:
:$a_3 / a_1 > 0$
that is:
:$a_1 a_3 > 0$
Thus, if $a_3^2 + a_1^2 a_4 = a_1 a_2 a_3$ and $a_1 a_3 > 0$, $Q$ has wholly imaginary roots.
Theorem: Soundness and Completeness of Semantic Tableaux

Let $\mathbf A$ be a WFF of propositional logic.
Let $T$ be a completed semantic tableau for $\mathbf A$.
Then $\mathbf A$ is unsatisfiable {{iff}} $T$ is closed.

Proof:
The two directions of this theorem are respectively addressed on:
:Soundness Theorem for Semantic Tableaux
:Completeness Theorem for Semantic Tableaux
{{qed}}
Theorem: Semantic Tableau Algorithm is Decision Procedure for Tautologies

The Semantic Tableau Algorithm is a decision procedure for tautologies.

Proof:
Let $\mathbf A$ be a WFF of propositional logic.
The Semantic Tableau Algorithm applied to $\neg \mathbf A$ yields a completed tableau for $\neg \mathbf A$.
By {{Corollary|Soundness and Completeness of Semantic Tableaux|2}}, this completed tableau decides if $\mathbf A$ is a tautology.
{{qed}}
Theorem: Soundness Theorem for Semantic Tableaux

Let $\mathbf A$ be a WFF of propositional logic.
Let $T$ be a completed tableau for $\mathbf A$.
Suppose that $T$ is closed.
Then $\mathbf A$ is unsatisfiable for boolean interpretations.

Proof:
We will prove inductively the following claim for every node $t$ of $T$:
:If all leaves that are descendants of $t$ are marked closed, then $\map U t$ is unsatisfiable.
By the Semantic Tableau Algorithm, we know this statement to hold for the leaf nodes themselves.
For, a leaf $t$ is marked closed {{iff}} $\map U t$ contains a complementary pair.
The assertion follows from Set of Literals Satisfiable iff No Complementary Pairs.
Inductively, suppose that all children of a node $t$ satisfy the mentioned condition.
If all descendant leaf nodes of $t$ are marked closed, this evidently holds for the children $t', t' '$ of $t$ as well.
Hence by hypothesis, $\map U {t'}$ and $\map U {t' '}$ are unsatisfiable.
Let $\mathbf B$ be the WFF used by the Semantic Tableau Algorithm at $t$.
Let $\mathbf B_1, \mathbf B_2$ be the formulas added to $t'$ and $t' '$.
First, the case that $\mathbf B$ is an $\alpha$-formula.
Then $t' = t' '$, and $\mathbf B$ is semantically equivalent to $\mathbf B_1 \land \mathbf B_2$.
It follows that if:
:$v \models_{\mathrm{BI}} \map U t$
for some boolean interpretation $v$, then also:
:$v \models_{\mathrm{BI}} \map U {t'}$
which contradicts our hypothesis.
Thus, $\map U t$ is unsatisfiable.
Next, the case that $\mathbf B$ is a $\beta$-formula.
Then $\mathbf B$ is semantically equivalent to $\mathbf B_1 \lor \mathbf B_2$.
It follows that if:
:$v \models_{\mathrm{BI}} \map U t$
for some boolean interpretation $v$, then also one of the following must hold:
:$v \models_{\mathrm{BI}} \map U {t'}$
:$v \models_{\mathrm{BI}} \map U {t' '}$
which contradicts our hypothesis.
Thus, $\map U t$ is unsatisfiable.
{{handwaving|"It follows", is obvious, and is tedious to write down}}
This proves our claim:
:If all leaves that are descendants of $t$ are marked closed, then $\map U t$ is unsatisfiable.
Applying this claim to the root node of $T$, we obtain the desired result.
{{qed}}
Theorem: Completeness Theorem for Semantic Tableaux

Let $\mathbf A$ be a WFF of propositional logic.
Let $\mathbf A$ be unsatisfiable for boolean interpretations.
Then every completed tableau for $\mathbf A$ is closed.

Proof:
{{AimForCont}} some open tableau $T$ for $\mathbf A$ exists.
We will prove that $\mathbf A$ must be satisfiable.
This claim is proved by inductively establishing the following claim for all nodes $t$ of $T$:
:If a descendant leaf node of $t$ is marked open, then $\map U t$ is satisfiable.
By the Semantic Tableau Algorithm, this statement is immediate for leaf nodes.
For, sought satisfiability is the condition for a leaf to be marked open.
Inductively suppose that all children of $t$ satisfy the mentioned condition.
Now suppose that $t$ has a descendant marked open leaf.
Then obviously some child $t'$ of $t$ also has a descendant marked open leaf.
By induction hypothesis, $\map U {t'}$ is satisfiable.
First, the case that the formula $\mathbf B$ used at $t$ by the Semantic Tableau Algorithm is an $\alpha$-formula.
Then $\map U {t'}$ is obtained from $\map U t$ by replacing $\mathbf B$ by $\mathbf B_1$ and $\mathbf B_2$.
Here, $\mathbf B_1$ and $\mathbf B_2$ are the formulas such that $\mathbf B$ is semantically equivalent to $\mathbf B_1 \land \mathbf B_2$.
It follows that if:
:$v \models_{\mathrm{BI}} \map U {t'}$
for some boolean interpretation $v$, then also:
:$v \models_{\mathrm{BI}} \map U t$
by the boolean interpretation of $\land$.
Consequently, $\map U t$ is satisfiable.
Next, the case that $\mathbf B$ is a $\beta$-formula.
Then $\mathbf B$ is semantically equivalent to $\mathbf B_1 \lor \mathbf B_2$.
Then, by the Rule of Addition:
:$\mathbf B_1 \models_{\mathrm{BI}} \mathbf B$
:$\mathbf B_2 \models_{\mathrm{BI}} \mathbf B$
Consequently, by the definitions of $\map U {t'}$ and $\map U {t' '}$:
{{explain|But $\map U {t' '}$ has not been defined}}
:$\map U {t'} \models_{\mathrm{BI}} \map U t$
:$\map U {t' '} \models_{\mathrm{BI}} \map U t$
By hypothesis, one of $\map U {t'}$ and $\map U {t' '}$ must be satisfiable.
Hence, so must $\map U t$ be.
This establishes our claim.
Applying the claim to the root node, that is, to the whole tableau, we obtain the result.
{{qed}}
Theorem: Cosine to Power of Even Integer/Proof 2

Let $n \in \Z$ be an even integer.
Then:
:$\ds \cos^n \theta = \frac 1 {2^{n - 1} } \sum_{k \mathop = 0}^{n / 2} \paren {\binom n k \cos \paren {n - 2 k} \theta}$
That is:
:$\cos^n \theta = \dfrac 1 {2^{n - 1} } \paren {\cos n \theta + n \cos \paren {n - 2} \theta + \dfrac {n \paren {n - 1} } 2 \cos \paren {n - 4} \theta + \cdots + \dfrac {n!} {\paren {\paren {\frac n 2}!}^2} \cos \theta}$

Proof:
{{begin-eqn}}
{{eqn | l = \cos^n \theta
      | r = \paren {\frac {e^{i \theta} + e^{-i \theta} } 2}^n
      | c = De Moivre's Theorem
}}
{{eqn | r = \frac {\paren {e^{i \theta} + e^{-i \theta} }^n} {2^n}
      | c = 
}}
{{eqn | r = \frac 1 {2^n} \sum_{k \mathop = 0}^n \binom n k e^{\paren {n - k} i \theta} e^{-k i \theta}
      | c = Binomial Theorem
}}
{{eqn | r = \frac 1 {2^n} \sum_{k \mathop = 0}^n \binom n k e^{\paren {n - 2 k} i \theta}
      | c = 
}}
{{end-eqn}}
Matching up terms from the beginning of this expansion with those from the end:
{{begin-eqn}}
{{eqn | l = 2^n \cos^n \theta
      | r = e^{n i \theta} + \binom n 1 e^{\paren {n - 2} i \theta} + \binom n 2 e^{\paren {n - 4} i \theta} + \cdots
      | c = 
}}
{{eqn | o =
      | ro= +
      | r = \binom n {n - 2} e^{-\paren {n - 4} i \theta} + \binom n {n - 1} e^{-\paren {n - 2} i \theta} + e^{-n i \theta}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {2^n} 2 \cos^n \theta
      | r = \paren {\frac {e^{n i \theta} + e^{-n i \theta} } 2} + \binom n 1 \paren {\frac {e^{\paren {n - 2} i \theta} + e^{-\paren {n - 2} i \theta} } 2}
      | c = 
}}
{{eqn | o =
      | ro= +
      | r = \binom n 2 \paren {\frac {e^{\paren {n - 4} i \theta} + e^{-\paren {n - 4} i \theta} } 2} + \cdots
      | c = 
}}
{{end-eqn}}
Thus:
:$\cos^n \theta = \dfrac 1 {2^{n - 1} } \paren {\cos n \theta + n \cos \paren {n - 2} \theta + \dfrac {n \paren {n - 1} } {2!} \cos \paren {n - 4} \theta + \cdots + R_n}$
Now to determine $R_n$.
The middle term of the sequence $0, 1, \ldots, n$ is $\dfrac n 2$.
So when $k = \dfrac n 2$ we have $n - 2k = 0$ and $n - k = n - \dfrac n 2 = \dfrac n 2$.
Thus:
{{begin-eqn}}
{{eqn | l = \binom n k
      | r = \frac {n!} {\paren {\paren {n / 2}!} \paren {\paren {n - n / 2}!} }
      | c = 
}}
{{eqn | r = \frac {n!} {\paren {\paren {n / 2}!}^2}
      | c = 
}}
{{end-eqn}}
So the middle term collapses to:
{{begin-eqn}}
{{eqn | l = R_n
      | r = 2 \frac {n!} {\paren {\paren {n / 2}!}^2} \frac {e^{0 i \theta} } 2
      | c = 
}}
{{eqn | r = \frac {n!} {\paren {\paren {n / 2}!}^2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Conjugate of Real Polynomial is Polynomial in Conjugate

Let $\map P z$ be a polynomial in a complex number $z$.
Let the coefficients of $P$ all be real.
Then:
:$\overline {\map P z} = \map P {\overline z}$
where $\overline z$ denotes the complex conjugate of $z$.

Proof:
Let $\map P z$ be expressed as:
:$a_n z^n + a_{n - 1} z^{n - 1} + \cdots + a_1 z + a_0$
Then:
{{begin-eqn}}
{{eqn | l = \overline {\map P z}
      | r = \overline {a_n z^n + a_{n-1} z^{n - 1} + \cdots + a_1 z + a_0}
      | c = 
}}
{{eqn | r = \overline {a_n z^n} + \overline {a_{n - 1} z^{n - 1} } + \cdots + \overline {a_1 z} + \overline {a_0}
      | c = Sum of Complex Conjugates
}}
{{eqn | r = \overline {a_n} \overline {z^n} + \overline {a_{n - 1} } \overline {z^{n - 1} } + \cdots + \overline {a_1} \overline z + \overline {a_0}
      | c = Product of Complex Conjugates
}}
{{eqn | r = a_n \overline {z^n} + a_{n - 1} \overline {z^{n - 1} } + \cdots + a_1 \overline z + a_0
      | c = Complex Number equals Conjugate iff Wholly Real
}}
{{eqn | r = a_n \overline z^n + a_{n - 1} \overline z^{n - 1} + \cdots + a_1 \overline z + a_0
      | c = Product of Complex Conjugates/General Result
}}
{{eqn | r = \map P {\overline z}
      | c = 
}}
{{end-eqn}}
{{qed}}