avewright/proofwiki-math huggingface dataset:
Theorem: Sum over k from 1 to n of n Choose k by Sine of n Theta

:$\ds \sum_{k \mathop = 1}^n \dbinom n k \sin k \theta = \paren {2 \cos \dfrac \theta 2}^n \sin \dfrac {n \theta} 2$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {1 + e^{i \theta} }^n
      | r = \sum_{k \mathop = 0}^n \dbinom n k e^{i k \theta}
      | c = Binomial Theorem
}}
{{eqn | r = \sum_{k \mathop = 0}^n \dbinom n k \paren {\cos k \theta + i \sin k \theta}
      | c = Euler's Formula
}}
{{eqn | ll= \leadsto
      | l = \map \Im {\paren {1 + e^{i \theta} }^n}
      | r = \map \Im {\sum_{k \mathop = 0}^n \dbinom n k \paren {\cos k \theta + i \sin k \theta} }
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^n \dbinom n k \sin k \theta
      | c = taking imaginary parts
}}
{{eqn | r = \sum_{k \mathop = 1}^n \dbinom n k \sin k \theta
      | c = as the zeroth term vanishes: $\sin 0 = 0$
}}
{{end-eqn}}
At the same time:
{{begin-eqn}}
{{eqn | l = \map \Im {\paren {1 + e^{i \theta} }^n}
      | r = \map \Im {e^{i n \theta / 2} \paren {e^{i \theta / 2} + e^{-i \theta / 2} }^n}
      | c = 
}}
{{eqn | r = \map \Im {e^{i n \theta / 2} \paren {2 \cos \dfrac \theta 2}^n}
      | c = Euler's Cosine Identity
}}
{{eqn | r = \map \Im {\paren {\cos \dfrac {n \theta} 2 + i \sin \dfrac {n \theta} 2} \paren {2 \cos \dfrac \theta 2}^n}
      | c = Euler's Formula
}}
{{eqn | r = \sin \dfrac {n \theta} 2 \paren {2 \cos \dfrac \theta 2}^n
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Point of Perpendicular Intersection on Real Line from Points in Complex Plane

Let $a, b \in \C$ be complex numbers represented by the points $A$ and $B$ respectively in the complex plane.
Let $x \in \R$ be a real number represented by the point $X$ on the real axis such that $AXB$ is a right triangle with $X$ as the right angle.
Then:
:$x = \dfrac {a_x - b_x \pm \sqrt {a_x^2 + b_x^2 + 2 a_x b_x - 4 a_y b_y} } 2$
where:
: $a = a_x + a_y i, b = b_x + b_y i$
{{mistake|What rubbish. Working on it.}}

Proof:
From Geometrical Interpretation of Complex Subtraction, the lines $XA$ and $XB$ can be represented by the complex numbers $a - x$ and $b - x$.
:400px
From Multiplication by Imaginary Unit is Equivalent to Rotation through Right Angle $a - x$ and $b - x$ are perpendicular {{iff}} either:
:$a - x = r i \paren {b - x}$
for some real numbers $r \in \R$.
That is, {{iff}} $\dfrac {a - x} {b - x}$ are purely imaginary.
Thus:
{{begin-eqn}}
{{eqn | l = \dfrac {a - x} {b - x}
      | r = r i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\paren {a - x} \paren {\overline b - x} } {\paren {b - x} \paren {\overline b - x} }
      | r = r i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {a_x + a_y i - x} \paren {b_x - b_y i - x}
      | r = r' i
      | c = for some $r' \in \R$: denominator is real
}}
{{eqn | ll= \leadsto
      | l = a_x b_x - a_x b_y i - a_x x + a_y b_x i + a_y b_y - a_y x i - x b_x - x b_y i + x^2
      | r = r' i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a_x b_x - a_x x + a_y b_y - x b_x + x^2
      | r = 0
      | c = equating real parts
}}
{{eqn | ll= \leadsto
      | l = x^2 - \paren {a_x + b_x} x + a_x b_x + a_y b_y
      | r = 0
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \dfrac {a_x + b_x \pm \sqrt {\paren {a_x + b_x}^2 - 4 \paren {a_x b_x + a_y b_y} } } 2
      | c = Quadratic Formula
}}
{{eqn | r = \dfrac {a_x + b_x \pm \sqrt {a_x^2 + b_x^2 + 2 a_x b_x - 4 a_x b_x - 4 a_y b_y} } 2
      | c = 
}}
{{eqn | r = \dfrac {a_x + b_x \pm \sqrt {a_x^2 + b_x^2 - 2 a_x b_x - 4 a_y b_y} } 2
      | c = 
}}
{{end-eqn}}
{{qed}}
{{Proofread|This did not work out as neatly as I expected. I may have made a mistake somewhere. The original example which inspired this page was a specific case where the numbers worked out neatly.}}
Theorem: Condition for Points in Complex Plane to form Parallelogram/Examples/2+i, 3+2i, 2+3i, 1+2i

The points in the complex plane represented by the complex numbers:
:$2 + i, 3 + 2 i, 2 + 3 i, 1 + 2 i$
are the vertices of a square.

Proof:
Let us label the points:
{{begin-eqn}}
{{eqn | l = A
      | o = :=
      | r = 2 + i
      | c = 
}}
{{eqn | l = B
      | o = :=
      | r = 3 + 2 i
      | c = 
}}
{{eqn | l = C
      | o = :=
      | r = 2 + 3 i
      | c = 
}}
{{eqn | l = D
      | o = :=
      | r = 1 + 2 i
      | c = 
}}
{{end-eqn}}
From Geometrical Interpretation of Complex Subtraction, we have that the difference $p - q$ between two complex numbers $p, q$ represents the vector $\vec {q p}$.
Let us take the differences of the complex numbers given:
{{begin-eqn}}
{{eqn | ll= B - A:
      | l = \paren{3 + 2 i} - \paren{2 + i}
      | r = 1 + i
      | c = 
}}
{{eqn | ll= B - C:
      | l = \paren{3 + 2 i} - \paren{2 + 3 i}
      | r = 1 - i
      | c = 
}}
{{eqn | ll= B - D:
      | l = \paren{3 + 2 i} - \paren{1 + 2 i}
      | r = 2 + 0 i
      | c = 
}}
{{eqn | ll= C - A:
      | l = \paren{2 + 3 i} - \paren{2 + i}
      | r = 0 + 2 i
      | c = 
}}
{{eqn | ll= C - D:
      | l = \paren{2 + 3 i} - \paren{1 + 2 i}
      | r = 1 + i
      | c = 
}}
{{eqn | ll= A - D:
      | l = \paren{2 + i} - \paren{1 + 2 i}
      | r = 1 - i
      | c = 
}}
{{end-eqn}}
So:
:$\vec {AB} = \vec {DC} = 1 + i$
:$\vec {DA} = \vec {CB} = 1 - i$
Thus by definition $ABCD$ forms a parallelogram.
Next it is noted that:
:$\paren {1 + i} i = i + i^2 = 1 - i$
and so $AB$ and $DC$ are perpendicular to $DA$ and $CB$.
Thus by definition $ABCD$ is a rectangle.
Finally note that:
:$\cmod {1 + i} = \cmod {1 - i} = \sqrt {1^2 + 1^2} = \sqrt 2$
and so:
:$\cmod {AB} = \cmod {DC} = \cmod {DC} = \cmod {DC}$
That is, all four sides of $ABCD$ are the same length.
Thus by definition $ABCD$ is a square.
{{qed}}
Theorem: Equation of Ellipse in Complex Plane

Let $\C$ be the complex plane.
Let $E$ be an ellipse in $\C$ whose major axis is $d \in \R_{>0}$ and whose foci are at $\alpha, \beta \in \C$.
Then $C$ may be written as:
:$\cmod {z - \alpha} + \cmod {z - \beta} = d$
where $\cmod {\, \cdot \,}$ denotes complex modulus.

Proof:
By definition of complex modulus:
:$\cmod {z - \alpha}$ is the distance from $z$ to $\alpha$
:$\cmod {z - \beta}$ is the distance from $z$ to $\beta$.
Thus $\cmod {z - \alpha} + \cmod {z - \beta}$ is the sum of the distance from $z$ to $\alpha$ and from $z$ to $\beta$.
This is precisely the equidistance property of the ellipse.
From Equidistance of Ellipse equals Major Axis, the constant distance $d$ is equal to the major axis of $E$.
{{qed}}
Theorem: Condition for Collinearity of Points in Complex Plane/Formulation 2

Let $z_1, z_2, z_3$ be distinct complex numbers.
Then:
:$z_1, z_2, z_3$ are collinear in the complex plane
{{iff}}:
::$\exists \alpha, \beta, \gamma \in \R: \alpha z_1 + \beta z_2 + \gamma z_3 = 0$
:where:
::$\alpha + \beta + \gamma = 0$
::not all of $\alpha, \beta, \gamma$ are zero.

Proof:
=== Sufficient Condition ===
Let $z_1, z_2, z_3$ be collinear.
Then by Condition for Collinearity of Points in Complex Plane: Formulation 1 there exists a real number $b$ such that:
:$z_2 - z_1 = b \paren {z_3 - z_1}$
Then:
{{begin-eqn}}
{{eqn | l = z_2 - z_1
      | r = b \paren {z_3 - z_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z_2 - z_1 - b z_3 + b z_1
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {b - 1} z_1 + z_2 - b z_3
      | r = 0
      | c = 
}}
{{end-eqn}}
Setting $\alpha = b - 1, \beta = 1, \gamma = -b$ fits the bill, as $\paren {b - 1} + 1 + \paren {-b} = 0$.
{{qed|lemma}}
Theorem: Quadrilateral in Complex Plane is Cyclic iff Cross Ratio of Vertices is Real

Let $z_1, z_2, z_3, z_4$ be distinct complex numbers.
Then:
:$z_1, z_2, z_3, z_4$ define the vertices of a cyclic quadrilateral
{{iff}} their cross-ratio:
:$\paren {z_1, z_3; z_2, z_4} = \dfrac {\paren {z_1 - z_2} \paren {z_3 - z_4} } {\paren {z_1 - z_4} \paren {z_3 - z_2} }$
is wholly real.

Proof:
Let $z_1 z_2 z_3 z_4$ be a cyclic quadrilateral.
By Geometrical Interpretation of Complex Subtraction, the four sides of $z_1 z_2 z_3 z_4$ can be defined as $z_1 - z_2$, $z_3 - z_2$, $z_3 - z_4$ and $z_1 - z_4$.
:400px
From Opposite Angles of Cyclic Quadrilateral sum to Two Right Angles, the opposite angles of $z_1 z_2 z_3 z_4$ sum to $\pi$ radians.
By Complex Multiplication as Geometrical Transformation, it follows that:
{{begin-eqn}}
{{eqn | l = \angle \, z_1
      | r = \map \arg {\dfrac {z_1 - z_2} {z_1 - z_4} }
      | c = 
}}
{{eqn | l = \angle \, z_2
      | r = \map \arg {\dfrac {z_3 - z_2} {z_1 - z_2} }
      | c = 
}}
{{eqn | l = \angle \, z_3
      | r = \map \arg {\dfrac {z_3 - z_4} {z_3 - z_2} }
      | c = 
}}
{{eqn | l = \angle \, z_4
      | r = \map \arg {\dfrac {z_1 - z_4} {z_3 - z_4} }
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \angle \, z_1 + \angle \, z_3
      | r = \pi
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \arg {\dfrac {z_1 - z_2} {z_1 - z_4} } + \arg \paren {\dfrac {z_3 - z_4} {z_3 - z_2} }
      | r = \pi
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \arg {\paren {\dfrac {z_1 - z_2} {z_1 - z_4} } \paren {\dfrac {z_3 - z_4} {z_3 - z_2} } }
      | r = \pi
      | c = Argument of Product equals Sum of Arguments
}}
{{eqn | ll= \leadsto
      | l = \map \Im {\dfrac {\paren {z_1 - z_2} \paren {z_3 - z_4} } {\paren {z_1 - z_4} \paren {z_3 - z_2} } }
      | r = 0
      | c = Argument of Negative Real Number is Pi
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Equation relating Points of Parallelogram in Complex Plane

Let $ABVU$ be a parallelogram in the complex plane whose vertices correspond to the complex numbers $a, b, v, u$ respectively.
Let $\angle BAU = \alpha$.
Let $\cmod {UA} = \lambda \cmod {AB}$.
:510px
Then:
:$u = \paren {1 - q} a + q b$
:$v = -q a + \paren {1 + q} b$
where:
:$q = \lambda e^{i \alpha}$

Proof:
From Geometrical Interpretation of Complex Subtraction, the four sides of $UABC$ can be defined as:
{{begin-eqn}}
{{eqn | l = UA
      | r = a - u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = AU
      | r = u - a
      | c = (easier in this form)
}}
{{eqn | l = AB
      | r = b - a
      | c = 
}}
{{eqn | l = UV
      | r = v - u
      | c = 
}}
{{eqn | l = BV
      | r = v - b
      | c = 
}}
{{end-eqn}}
Thus: 
{{begin-eqn}}
{{eqn | l = UA
      | r = \lambda \paren {AB}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cmod {a - u}
      | r = \lambda \cmod {b - a}
      | c = 
}}
{{eqn | l = BAU
      | r = \alpha
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \alpha + \map \arg {b - a}
      | r = \map \arg {u - a}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = u - a
      | r = \lambda e^{i \alpha} \paren {b - a}
      | c = Product of Complex Numbers in Exponential Form
}}
{{eqn | ll= \leadsto
      | l = u
      | r = a + q \paren {b - a}
      | c = where $q = \lambda e^{i \alpha}$
}}
{{eqn | r = \paren {1 - q} a + q b 
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Then we have:
{{begin-eqn}}
{{eqn | l = v - u
      | r = b - a
      | c = Opposite Sides and Angles of Parallelogram are Equal
}}
{{eqn | ll= \leadsto
      | l = v
      | r = u + b - a
      | c = 
}}
{{eqn | r = \paren {1 - q} a + q b + b - a
      | c = 
}}
{{eqn | r = -q a + \paren {1 + q} b
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Circle of Apollonius in Complex Plane

Let $\C$ be the complex plane.
Let $\lambda \in \R$ be a real number such that $\lambda \ne 0$ and $\lambda \ne 1$.
Let $a, b \in \C$ such that $a \ne b$.
The equation:
:$\cmod {\dfrac {z - a} {z - b} } = \lambda$
decribes a circle of Apollonius $C$ in $\C$ such that:
:if $\lambda < 0$, then $a$ is inside $C$ and $b$ is outside
:if $\lambda > 0$, then $b$ is inside $C$ and $a$ is outside.
If $\lambda = 1$ then $z$ describes the perpendicular bisector of the line segment joining $a$ to $b$.

Proof:
By the geometry, the locus described by this equation is a circle of Apollonius.
{{finish|etc.}}
Theorem: Circle of Apollonius in Complex Plane

Let $\C$ be the complex plane.
Let $\lambda \in \R$ be a real number such that $\lambda \ne 0$ and $\lambda \ne 1$.
Let $a, b \in \C$ such that $a \ne b$.
The equation:
:$\cmod {\dfrac {z - a} {z - b} } = \lambda$
decribes a circle of Apollonius $C$ in $\C$ such that:
:if $\lambda < 0$, then $a$ is inside $C$ and $b$ is outside
:if $\lambda > 0$, then $b$ is inside $C$ and $a$ is outside.
If $\lambda = 1$ then $z$ describes the perpendicular bisector of the line segment joining $a$ to $b$.

Proof:
A point $P$ on this circle is $2$ times the distance from $z = 3$ as it is from $z = -3$.
:thumb400px
Let $z = x + i y$.
{{begin-eqn}}
{{eqn | l = \cmod {\dfrac {z - 3} {z + 3} }
      | r = 2
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \cmod {z - 3}
      | r = 2 \cmod {z + 3}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \cmod {x + i y - 3}
      | r = 2 \cmod {x + i y + 3}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \sqrt {\paren {x - 3}^2 + y^2}
      | r = 2 \sqrt {\paren {x + 3}^2 + y^2}
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {x - 3}^2 + y^2
      | r = 4 \paren {\paren {x + 3}^2 + y^2}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x^2 - 6 x + 9 + y^2
      | r = 4 x^2 + 24 x + 36 + 4 y^2
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = 3 x^2 + 30 x + 27 + 3 y^2
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x^2 + 10 x + 9 + y^2
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {x + 5}^2 - 25 + 9 + y^2
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {x + 5}^2 + y^2
      | r = 16
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \cmod {z + 5}
      | r = 4
      | c = 
}}
{{end-eqn}}
Hence the result by Equation of Circle in Complex Plane.
{{Qed}}
Theorem: Circle of Apollonius in Complex Plane

Let $\C$ be the complex plane.
Let $\lambda \in \R$ be a real number such that $\lambda \ne 0$ and $\lambda \ne 1$.
Let $a, b \in \C$ such that $a \ne b$.
The equation:
:$\cmod {\dfrac {z - a} {z - b} } = \lambda$
decribes a circle of Apollonius $C$ in $\C$ such that:
:if $\lambda < 0$, then $a$ is inside $C$ and $b$ is outside
:if $\lambda > 0$, then $b$ is inside $C$ and $a$ is outside.
If $\lambda = 1$ then $z$ describes the perpendicular bisector of the line segment joining $a$ to $b$.

Proof:
{{begin-eqn}}
{{eqn | l = \cmod {\dfrac {z - 3} {z + 3} }
      | r = 2
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {\dfrac {z - 3} {z + 3} } \paren {\dfrac {\overline z - 3} {\overline z + 3} }
      | r = 4
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = z \overline z + 5 \overline z + 5 z + 9
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {z + 5} \paren {\overline z + 5}
      | r = 16
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \cmod {z + 5}
      | r = 4
      | c = 
}}
{{end-eqn}}
Hence the result by Equation of Circle in Complex Plane.
{{Qed}}
Theorem: Circle of Apollonius is Circle

Let $A, B$ be distinct points in the plane.
Let $\lambda \in \R_{>0}$ be a strictly positive real number.
Let $X$ be the locus of points in the plane such that:
:$XA = \lambda \paren {XB}$
Then $X$ is in the form of a circle, known as a circle of Apollonius.
:400px
If $\lambda < 1$, then $A$ is inside the circle, and $B$ is outside.
If $\lambda > 1$, then $B$ is inside the circle, and $A$ is outside.

Proof:
:340px
Let $P$ be an arbitrary point such that $\dfrac {AP} {PB} = \lambda$.
Let $\angle APB$ be bisected internally and externally to intersect $AB$ at $X$ and $Y$ respectively.
Then by Angle Bisector Theorem:
:$\dfrac {AX} {XB} = \dfrac {AP} {PB} = \lambda$
and by Angle Bisector Theorem (Exterior Angle):
:$\dfrac {AY} {YB} = \dfrac {AP} {PB} = \lambda$
Thus $X$ and $Y$ are the points which divide $AB$ internally and externally in the given ratio.
Therefore, for a given $A$, $B$ and $\lambda$, $X$ and $Y$ are fixed.
From Bisectors of Adjacent Angles between Straight Lines Meeting at Point are Perpendicular, $\angle XPY$ is a right angle.
Hence by Thales' Theorem, $P$ lies on the circumference of a circle of which $XY$ is a diameter.
{{qed}}
Theorem: Sextuple Angle Formulas/Cosine

:$\cos 6 \theta = 32 \cos^6 \theta - 48 \cos^4 \theta + 18 \cos^2 \theta - 1$

Proof:
{{begin-eqn}}
{{eqn | l = \cos 6 \theta + i \sin 6 \theta
      | r = \paren {\cos \theta + i \sin \theta}^6
      | c = De Moivre's Formula
}}
{{eqn | r = \paren {\cos \theta}^6 + \binom 6 1 \paren {\cos \theta}^5 \paren {i \sin \theta} + \binom 6 2 \paren {\cos \theta}^4 \paren {i \sin \theta}^2
      | c = Binomial Theorem
}}
{{eqn | o = 
      | ro=+
      | r = \binom 6 3 \paren {\cos \theta}^3 \paren {i \sin \theta}^3 + \binom 6 4 \paren {\cos \theta}^2 \paren {i \sin \theta}^4 + \binom 6 5 \paren {\cos \theta} \paren {i \sin \theta}^5 + \paren {i \sin \theta}^6
}}
{{eqn | r = \cos^6 \theta + 6 i \cos^5 \theta \sin \theta - 15 \cos^4 \sin^2 \theta
      | c = substituting for binomial coefficients
}}
{{eqn | o = 
      | ro=-
      | r = 20 i \cos^3 \theta \sin^3 \theta + 15 \cos^2 \theta \sin^4 \theta + 6 i \cos \theta \sin^5 \theta - \sin^6 \theta
      | c = and using $i^2 = -1$
}}
{{eqn | n = 1
      | r = \cos^6 \theta - 15 \cos^4 \sin^2 \theta + 15 \cos^2 \theta \sin^4 \theta - \sin^6 \theta
}}
{{eqn | o = 
      | ro=+
      | r = i \paren {6 \cos^5 \theta \sin \theta - 20 \cos^3 \theta \sin^3 \theta + 6 \cos \theta \sin^5 \theta}
      | c = rearranging
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \cos 6 \theta
      | r = \cos^6 \theta - 15 \cos^4 \sin^2 \theta + 15 \cos^2 \theta \sin^4 \theta - \sin^6 \theta
      | c = equating real parts in $(1)$
}}
{{eqn | r = \cos^6 \theta - 15 \cos^4 \paren {1 - \cos^2 \theta} + 15 \cos^2 \theta \paren {1 - \cos^2 \theta}^2 \theta -  \paren {1 - \cos^2 \theta}^3
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = 32 \cos^6 \theta - 48 \cos^4 \theta + 18 \cos^2 \theta - 1
      | c = multiplying out and gathering terms
}}
{{end-eqn}}
{{qed}}
Theorem: Sextuple Angle Formulas/Sine

:$\dfrac {\sin 6 \theta} {\sin \theta} = 32 \cos^5 \theta - 32 \cos^3 \theta + 6 \cos \theta$

Proof:
{{begin-eqn}}
{{eqn | l = \cos 6 \theta + i \sin 6 \theta
      | r = \paren {\cos \theta + i \sin \theta}^6
      | c = De Moivre's Formula
}}
{{eqn | r = \paren {\cos \theta}^6 + \binom 6 1 \paren {\cos \theta}^5 \paren {i \sin \theta} + \binom 6 2 \paren {\cos \theta}^4 \paren {i \sin \theta}^2
      | c = Binomial Theorem
}}
{{eqn | o = 
      | ro=+
      | r = \binom 6 3 \paren {\cos \theta}^3 \paren {i \sin \theta}^3 + \binom 6 4 \paren {\cos \theta}^2 \paren {i \sin \theta}^4 + \binom 6 5 \paren {\cos \theta} \paren {i \sin \theta}^5 + \paren {i \sin \theta}^6
}}
{{eqn | r = \cos^6 \theta + 6 i \cos^5 \theta \sin \theta - 15 \cos^4 \sin^2 \theta
      | c = substituting for binomial coefficients
}}
{{eqn | o = 
      | ro=-
      | r = 20 i \cos^3 \theta \sin^3 \theta + 15 \cos^2 \theta \sin^4 \theta + 6 i \cos \theta \sin^5 \theta - \sin^6 \theta
      | c = and using $i^2 = -1$
}}
{{eqn | n = 1
      | r = \cos^6 \theta - 15 \cos^4 \sin^2 \theta + 15 \cos^2 \theta \sin^4 \theta - \sin^6 \theta
}}
{{eqn | o = 
      | ro=+
      | r = i \paren {6 \cos^5 \theta \sin \theta - 20 \cos^3 \theta \sin^3 \theta  + 6 \cos \theta \sin^5 \theta}
      | c = rearranging
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \sin 6 \theta
      | r = 6 \cos^5 \theta \sin \theta - 20 \cos^3 \theta \sin^\theta + 6 \cos \theta \sin^5 \theta
      | c = equating imaginary parts in $(1)$
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\map \sin {6 \theta} } {\sin \theta}
      | r = 6 \cos^5 \theta - 20 \cos^3 \theta \sin^2 \theta + 6 \cos \theta \sin^4 \theta
      | c = 
}}
{{eqn | r = 6 \cos^5 \theta - 20 \cos^3 \theta \paren {1 - \cos^2 \theta} + 6 \cos \theta \paren {1 - \cos^2 \theta}^2
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = 32 \cos^5 \theta - 32 \cos^3 \theta + 6 \cos \theta
      | c = multiplying out and gathering terms
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of Angle plus Integer Multiple of Pi

:$\map \cos {\theta + n \pi} = \paren {-1}^n \cos \theta$

Proof:
{{begin-eqn}}
{{eqn | l = \map \cos {\theta + n \pi}
      | r = \cos \theta \cos n \pi - \sin \theta \sin n \pi
      | c = Cosine of Sum
}}
{{eqn | r = \cos \theta \cos n \pi
      | c = Sine of Integer Multiple of Pi
}}
{{eqn | r = \paren {-1}^n \cos \theta
      | c = Cosine of Integer Multiple of Pi
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Angle plus Integer Multiple of Pi

:$\map \sin {\theta + n \pi} = \paren {-1}^n \sin \theta$

Proof:
{{begin-eqn}}
{{eqn | l = \map \sin {\theta + n \pi}
      | r = \sin \theta \cos n \pi + \cos \theta \sin n \pi
      | c = Sine of Sum
}}
{{eqn | r = \sin \theta \cos n \pi
      | c = Sine of Integer Multiple of Pi
}}
{{eqn | r = \paren {-1}^n \sin \theta
      | c = Cosine of Integer Multiple of Pi
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Division/Examples/(1 + sin theta + i cos theta) (1 + sin theta - i cos theta)^-1

:$\dfrac {1 + \sin \theta + i \cos \theta} {1 + \sin \theta - i \cos \theta} = \sin \theta + i \cos \theta$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {1 + \sin \theta + i \cos \theta} {1 + \sin \theta - i \cos \theta}
      | r = \frac {\paren {1 + \sin \theta + i \cos \theta}^2} {\paren {1 + \sin \theta - i \cos \theta} \paren {1 + \sin \theta + i \cos \theta} }
      | c = 
}}
{{eqn | r = \frac {\paren {1 + \sin \theta}^2 + 2 i \cos \theta \paren {1 + \sin \theta} - \cos^2 \theta} {\paren {1 + \sin \theta}^2 + \cos^2 \theta}
      | c = 
}}
{{eqn | r = \frac {1 + 2 \sin \theta + \sin^2 \theta + 2 i \cos \theta \paren {1 + \sin \theta} - \cos^2 \theta} {1 + 2 \sin \theta + \sin^2 \theta + \cos^2 \theta}
      | c = 
}}
{{eqn | r = \frac {1 + 2 \sin \theta + 2 \sin^2 \theta + 2 i \cos \theta \paren {1 + \sin \theta} - \paren {\cos^2 \theta + \sin^2 \theta} } {1 + 2 \sin \theta + \sin^2 \theta + \cos^2 \theta}
      | c = 
}}
{{eqn | r = \frac {2 \sin \theta \paren {1 + \sin \theta} + 2 i \cos \theta \paren {1 + \sin \theta} } {2 + 2 \sin \theta}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \sin \theta + i \cos \theta
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of 1 + sin pi by 5 plus i cos pi by 5 to Fifth Power plus i times its Conjugate

:$\paren {1 + \sin \dfrac \pi 5 + i \cos \dfrac \pi 5}^5 + i \paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5 = 0$

Proof:
{{begin-eqn}}
{{eqn | r = \paren {1 + \sin \dfrac \pi 5 + i \cos \dfrac \pi 5}^5 + i \paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5
      | o = 
      | c = 
}}
{{eqn | r = \frac {\paren {1 + \sin \dfrac \pi 5 + i \cos \dfrac \pi 5}^5} {\paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5} \paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5 + i \paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5
      | c = 
}}
{{eqn | r = \paren {\sin \dfrac \pi 5 + i \cos  \dfrac \pi 5}^5 \paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5 + i \paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5
      | c = Complex Division Examples: $\dfrac {1 + \sin \theta + i \cos \theta} {1 + \sin \theta - i \cos \theta}$
}}
{{eqn | r = i^5 \paren {-i \sin \dfrac \pi 5 + \cos  \dfrac \pi 5}^5 \paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5 + i \paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5
      | c = multiplying left hand term by $i^5 \times -i = 1$
}}
{{eqn | r = i \paren {\cos \pi - i \sin \pi} \paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5 + i \paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5
      | c = De Moivre's Formula
}}
{{eqn | r = i \paren {-1} \paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5 + i \paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5
      | c = Sine of Straight Angle and Cosine of Straight Angle
}}
{{eqn | r = -i \paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5 + i \paren {1 + \sin \dfrac \pi 5 - i \cos \dfrac \pi 5}^5
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
Theorem: Complex Roots of Unity include 1

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $U_n = \set {z \in \C: z^n = 1}$ be the set of complex $n$th roots of unity.
Then $1 \in U_n$.
That is, $1$ is always one of the complex $n$th roots of unity of any $n$.

Proof:
By definition of integer power:
:$1^n = 1$
for all $n$.
Hence the result.
{{qed}}