avewright/proofwiki-math huggingface dataset:
Theorem: Equation of Circle in Complex Plane/Formulation 2

Let $\C$ be the complex plane.
Let $C$ be a circle in $\C$.
Then $C$ may be written as:
:$\alpha z \overline z + \beta z + \overline \beta \overline z + \gamma = 0$
where:
:$\alpha \in \R_{\ne 0}$ is real and non-zero
:$\gamma \in \R$ is real
:$\beta \in \C$ is complex such that $\cmod \beta^2 > \alpha \gamma$.
The curve $C$ is a straight line {{iff}} $\alpha = 0$ and $\beta \ne 0$.

Proof:
From Equation of Circle in Cartesian Plane: Formulation 2, the equation for a circle is:
:$A \paren {x^2 + y^2} + B x + C y + D = 0$
provided that:
:$B^2 + C^2 \ge 4 A D$
:$A > 0$.
Thus:
{{begin-eqn}}
{{eqn | l = A \paren {x^2 + y^2} + B x + C y + D
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A z \overline z + B x + C y + D
      | r = 0
      | c = Product of Complex Number with Conjugate
}}
{{eqn | ll= \leadsto
      | l = A z \overline z + \frac B 2 \paren {z + \overline z} + C y + D
      | r = 0
      | c = Sum of Complex Number with Conjugate
}}
{{eqn | ll= \leadsto
      | l = A z \overline z + \frac B 2 \paren {z + \overline z} + \frac C {2 i} \paren {z - \overline z} + D
      | r = 0
      | c = Difference of Complex Number with Conjugate
}}
{{eqn | ll= \leadsto
      | l = A z \overline z + \paren {\frac B 2 + \frac C {2 i} } z + \paren {\frac B 2 - \frac C {2 i} } \overline z + D
      | r = 0
      | c = gathering terms
}}
{{end-eqn}}
By setting:
:$\alpha := A$, $\beta := \dfrac B 2 + \dfrac C {2 i}$ and $\gamma := D$
we have:
:$\alpha z \overline z + \beta z + \overline \beta \overline z + \gamma = 0$
As $A, B, C, D \in \R$ it follows that both $\alpha$ and $\gamma$ are real.
Then we have that $A > 0$ and so $\alpha > 0$.
Then note that:
{{begin-eqn}}
{{eqn | l = \paren {\frac B 2 + \frac C {2 i} } \paren {\frac B 2 - \frac C {2 i} }
      | r = \paren {\frac B 2}^2 + \paren {\frac C 2}^2
      | c = 
}}
{{eqn | r = \frac {B^2 + C^2} 4
      | c = 
}}
{{end-eqn}}
Given that:
:$B^2 + C^2 \ge 4 A D$
it follows that:
:$\cmod \beta^2 > \alpha \gamma$
{{qed|lemma}}
If $\alpha = 0$ and $\beta \ne 0$ the equation devolves to:
:$\beta z + \overline \beta \overline z + \gamma = 0$
which from Equation of Line in Complex Plane: Formulation 1 is the equation of a straight line.
The result follows.
{{qed}}
Theorem: Equation of Line in Complex Plane/Formulation 1

Let $\C$ be the complex plane.
Let $L$ be a straight line in $\C$.
Then $L$ may be written as:
:$\beta z + \overline \beta \overline z  + \gamma = 0$
where $\gamma$ is real and $\beta$ may be complex.

Proof:
From Equation of Straight Line in Plane, the equation for a straight line is:
:$A x + B y + C = 0$
Thus:
{{begin-eqn}}
{{eqn | l = A x + B y + C
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac A 2 \paren {z + \overline z} + B y + C
      | r = 0
      | c = Sum of Complex Number with Conjugate
}}
{{eqn | ll= \leadsto
      | l = \frac A 2 \paren {z + \overline z} + \frac B {2 i} \paren {z - \overline z} + C
      | r = 0
      | c = Difference of Complex Number with Conjugate
}}
{{eqn | ll= \leadsto
      | l = \paren {\frac A 2 + \frac B {2 i} } z + \paren {\frac A 2 - \frac B {2 i} } \overline z + C
      | r = 0
      | c = gathering terms
}}
{{end-eqn}}
The result follows by setting $\beta := \dfrac A 2 + \dfrac B {2 i}$ and $\gamma := C$.
{{qed}}
Theorem: Vertices of Equilateral Triangle in Complex Plane

Let $z_1$, $z_2$ and $z_3$ be complex numbers.
Then:
: $z_1$, $z_2$ and $z_3$ represent on the complex plane the vertices of an equilateral triangle
{{iff}}:
:${z_1}^2 + {z_2}^2 + {z_3}^2 = z_1 z_2 + z_2 z_3 + z_3 z_1$

Proof:
:400px
Theorem: Product of Sines of Fractions of Pi

Let $m \in \Z$ such that $m > 1$.
Then:
:$\ds \prod_{k \mathop = 1}^{m - 1} \sin \frac {k \pi} m = \frac m {2^{m - 1} }$

Proof:
From Product Formula for Sine, we have:
:$\ds \map \sin {n z} = 2^{n - 1} \prod_{k \mathop = 0}^{n - 1} \map \sin {z + \frac {k \pi} n}$
Therefore:
{{begin-eqn}}
{{eqn | l = \map \sin {n z}
      | r = 2^{n - 1} \prod_{k \mathop = 0}^{n - 1} \map \sin {z + \frac {k \pi} n}
      | c = 
}}
{{eqn | r = 2^{n - 1} \map \sin z \prod_{k \mathop = 1}^{n - 1} \map \sin {z + \frac {k \pi} n}
      | c = extracting $\map \sin z$
}}
{{eqn | ll= \leadsto
      | l = \frac {\map \sin {n z} } {\map \sin z}
      | r = 2^{n - 1} \prod_{k \mathop = 1}^{n - 1} \map \sin {z + \frac {k \pi} n}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\map \sin {n z} } {\map \sin z} \times \frac z {n z}
      | r = \frac z {n z} \times 2^{n - 1} \prod_{k \mathop = 1}^{n - 1} \map \sin {z + \frac {k \pi} n}
      | c = multiplying both sides by $\dfrac z {n z}$
}}
{{eqn | ll= \leadsto
      | l = \lim_{z \mathop \to 0} \dfrac {\dfrac {\map \sin {n z} } {n z} } {\dfrac {\map \sin z} z }
      | r = \lim_{z \mathop \to 0} \frac 1 n \times 2^{n - 1} \prod_{k \mathop = 1}^{n - 1} \map \sin {z + \frac {k \pi} n}
      | c = taking the limit of both sides
}}
{{eqn | ll= \leadsto
      | l = 1
      | r = \frac 1 n \times 2^{n - 1} \prod_{k \mathop = 1}^{n - 1} \map \sin {\frac {k \pi} n}
      | c = Limit of $\dfrac {\sin x} x$ at Zero
}}
{{eqn | ll= \leadsto
      | l = \prod_{k \mathop = 1}^{n - 1} \map \sin {\frac {k \pi} n}
      | r = \frac n {2^{n - 1} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Complex Conjugates/General Result

Let $z_1, z_2, \ldots, z_n \in \C$ be complex numbers.
Let $\overline z$ be the complex conjugate of the complex number $z$.
Then:
:$\ds \overline {\prod_{j \mathop = 1}^n z_j} = \prod_{j \mathop = 1}^n \overline {z_j}$

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\ds \overline {\prod_{j \mathop = 1}^n z_j} = \prod_{j \mathop = 1}^n \overline {z_j}$
$\map P 1$ is trivially true, as this just says $\overline {z_1} = \overline {z_1}$.
Theorem: Quotient of Complex Conjugates

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\overline z$ be the complex conjugate of the complex number $z$.
Then:
:$\overline {\paren {\dfrac {z_1} {z_2} } } = \dfrac {\paren {\overline {z_1} } } {\paren {\overline {z_2} } }$
for $z_2 \ne 0$.

Proof:
Let $z_1 = x_1 + i y_1$ and $z_2 = x_2 + i y_2$, where $x_1, y_1, x_2, y_2 \in \R$.
Then:
{{begin-eqn}}
{{eqn | l = \overline {\paren {\frac {z_1} {z_2} } }
      | r = \overline {\paren {\frac {x_1 x_2 + y_1 y_2} { {x_2}^2 + {y_2}^2} + i \frac {x_2 y_1 - x_1 y_2} { {x_2}^2 + {y_2}^2} } } 
      | c = Division of Complex Numbers
}}
{{eqn | r = \frac {x_1 x_2 + y_1 y_2} { {x_2}^2 + {y_2}^2} - i \frac {x_2 y_1 - x_1 y_2} { {x_2}^2 + {y_2}^2}
      | c = {{Defof|Complex Conjugate}}
}}
{{eqn | r = \frac {x_1 x_2 + \paren {-y_1} \paren {-y_2} } { {x_2}^2 + \paren {-y_2}^2} + i \frac {x_2 \paren {-y_1} - x_1 \paren {-y_2} } { {x_2}^2 + \paren {-y_2}^2}
      | c = 
}}
{{eqn | r = \frac {x_1 - i y_1} {x_2 - i y_2}
      | c = Division of Complex Numbers
}}
{{eqn | r = \frac {\paren {\overline {z_1} } } {\paren {\overline {z_2} } }
      | c = {{Defof|Complex Conjugate}}
}}
{{end-eqn}}
{{qed}}
Theorem: Condition for Points in Complex Plane to form Parallelogram

Let $A = z_1$, $B = z_2$, $C = z_3$ and $D = z_4$ represent on the complex plane the vertices of a quadrilateral.
Then $ABCD$ is a parallelogram {{iff}}:
:$z_1 - z_2 + z_3 - z_4 = 0$

Proof:
:400px
$ABCD$ is a parallelogram {{iff}}:
:$\vec {AB} = \vec {DC}$
Then:
{{begin-eqn}}
{{eqn | l = \vec {AB}
      | r = \vec {DC}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = z_2 - z_1
      | r = z_3 - z_4
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = z_1 - z_2 + z_3 - z_4
      | r = 0
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Quadrilateral with Bisecting Diagonals is Parallelogram

Let $ABCD$ be a quadrilateral.
Let the diagonals of $ABCD$ bisect each other.
Then $ABCD$ is a parallelogram.

Proof:
The diagonals of $ABCD$ bisect each other if the position vectors of the midpoints of the diagonals are the same point.
Let $z_1, z_2, z_3, z_4$ be the position vectors of the vertices of $ABCD$.
Thus:
{{begin-eqn}}
{{eqn | l = z_1 + \frac {z_3 - z_1} 2
      | r = z_2 + \frac {z_4 - z_2} 2
      | c = condition for bisection
}}
{{eqn | ll= \leadsto
      | l = \frac {z_1 + z_3} 2
      | r = \frac {z_2 + z_4} 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z_1 + z_3
      | r = z_2 + z_4
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z_1 - z_2 + z_3 - z_4
      | r = 0
      | c = 
}}
{{end-eqn}}
The result follows from Condition for Points in Complex Plane to form Parallelogram.
{{qed}}
Theorem: Medians of Triangle Meet at Centroid

Let $\triangle ABC$ be a triangle.
Then the medians of $\triangle ABC$ meet at a single point.
This point is called the centroid of $\triangle ABC$.

Proof:
:360px
Let $A'$ be the midpoint of $BC$.
Let $B'$ be the midpoint of $AC$.
Let $C'$ be the midpoint of $AB$.
Hence $AA'$, $BB'$ and $CC'$ are the medians of $\triangle ABC$.
Let $AA'$ and $BB'$ intersect at $G$.
Hence $A'B'$ is a midline of $\triangle ABC$.
By the Midline Theorem, $A'B'$ is parallel to $AB$ and half the length of $AB$.
We have that $\triangle AGB$ and $\triangle A'GB'$ are similar.
Hence:
{{begin-eqn}}
{{eqn | l = A'G
      | r = \dfrac {AG} 2
}}
{{eqn | l = B'G
      | r = \dfrac {BG} 2
}}
{{end-eqn}}
Hence $BB'$ meets $AA'$ $\dfrac 1 3$ of the length along $AA'$ from $A'$.
That is:
:$A'G = \dfrac {AA'} 3$
Similarly, {{mutatis}}, it can be shown that $CC'$ also meets $AA'$ $\dfrac 1 3$ of the length along $AA'$ from $A'$.
Hence we have shown that $BB'$ and $CC'$ both meet at the same point on $AA'$
That is, the medians of $\triangle ABC$ meet at a single point.
Theorem: Midpoints of Sides of Quadrilateral form Parallelogram

Let $\Box ABCD$ be a quadrilateral.
Let $E, F, G, H$ be the midpoints of $AB, BC, CD, DA$ respectively.
Then $\Box EFGH$ is a parallelogram.

Proof:
Let $z_1, z_2, z_3, z_4$ be the position vectors of the vertices of $\Box ABCD$.
The midpoints of the sides of $\Box ABCD$ are, then:
{{begin-eqn}}
{{eqn | l = OE
      | r = \frac {z_1 + z_2} 2
      | c = 
}}
{{eqn | l = OF
      | r = \frac {z_2 + z_3} 2
      | c = 
}}
{{eqn | l = OG
      | r = \frac {z_3 + z_4} 2
      | c = 
}}
{{eqn | l = OH
      | r = \frac {z_4 + z_1} 2
      | c = 
}}
{{end-eqn}}
Take two opposite sides $EF$ and $HG$:
{{begin-eqn}}
{{eqn | l = EF
      | r = \frac {z_2 + z_3} 2 - \frac {z_1 + z_2} 2
      | c = 
}}
{{eqn | r = \frac {z_3} 2 - \frac {z_1} 2
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = HG
      | r = \frac {z_3 + z_4} 2 - \frac {z_4 + z_1} 2
      | c = 
}}
{{eqn | r = \frac {z_3} 2 - \frac {z_1} 2
      | c = 
}}
{{eqn | r = EF
      | c = 
}}
{{end-eqn}}
The vectors defining the opposite sides of $\Box EFGH$ are equal.
The result follows by definition of parallelogram.
{{qed}}
Theorem: Line from Bisector of Side of Parallelogram to Vertex Trisects Diagonal

Let $ABCD$ be a parallelogram.
Let $E$ be the midpoint of $AD$.
Then the point at which the line $BE$ meets $AC$ trisects $AC$.

Proof:
:400px
Let the given intersection be at $F$.
We have that $E$ is the midpoint of $AD$.
Thus:
{{begin-eqn}}
{{eqn | l = \vec {AB} + \vec {BE}
      | r = \frac {\vec {AD} } 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \vec {BE}
      | r = \frac {\vec {AD} } 2 - \vec {AB}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \vec {AF}
      | r = m \paren {\frac {\vec {AD} } 2 - \vec {BE} }
      | c = for some $m$ such that $0 \le m \le 1$
}}
{{end-eqn}}
Since $\vec {AB} + \vec {BC}$ we have $\vec {AF} = n \paren {\vec {AB} + \vec {BC} }$ where $0 \le n \le 1$.
But:
:$\vec {AB} + \vec {BF} = \vec {AF}$
That is:
:$\vec {AB} + m \paren {\dfrac {\vec {BC} } 2 - \vec {AB} } = n \paren {\vec {AB} + \vec {BC} }$
That is:
:$\paren {1 - m - n} \vec {AB} + \paren {\dfrac m 2 - n} \vec {AB} = 0$
These have a simultaneous solution because $\vec {AB}$ and $\vec {AD}$ are neither coincident nor parallel.
So:
:$1 - m - n = 0, \dfrac m 2 - n = 0 \implies m = 2 n$
Hence $3n = 1$ and so:
:$n = \dfrac 1 3$
{{qed}}
Theorem: Sum of Complex Numbers in Exponential Form

Let $z_1 = r_1 e^{i \theta_1}$ and $z_2 = r_2 e^{i \theta_2}$ be complex numbers expressed in exponential form.
Let $z_3 = r_3 e^{i \theta_3} = z_1 + z_2$.
Then:
:$r_3 = \sqrt { {r_1}^2 + {r_2}^2 + 2 r_1 r_2 \map \cos {\theta_1 - \theta_2} }$
:$\theta_3 = \map \arctan {\dfrac {r_1 \sin \theta_1 + r_2 \sin \theta_2} {r_1 \cos \theta_1 + r_2 \cos \theta_2} }$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = r_1 e^{i \theta_1} + r_2 e^{i \theta_2}
      | r = r_1 \paren {\cos \theta_1 + i \sin \theta_1} + r_2 \paren {\cos \theta_2 + i \sin \theta_2}
      | c = {{Defof|Polar Form of Complex Number}}
}}
{{eqn | r = \paren {r_1 \cos \theta_1 + r_2 \cos \theta_2} + i \paren {r_1 \sin \theta_1 + r_2 \sin \theta_2}
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = {r_3}^2
      | r = {r_1}^2 + {r_2}^2 + 2 r_1 r_2 \map \cos {\theta_1 - \theta_2}
      | c = Complex Modulus of Sum of Complex Numbers
}}
{{eqn | ll= \leadsto
      | l = r_3
      | r = \sqrt { {r_1}^2 + {r_2}^2 + 2 r_1 r_2 \map \cos {\theta_1 - \theta_2} }
      | c = 
}}
{{end-eqn}}
and similarly:
:$\theta_3 = \map \arctan {\dfrac {r_1 \sin \theta_1 + r_2 \sin \theta_2} {r_1 \cos \theta_1 + r_2 \cos \theta_2} }$
{{qed}}
Theorem: De Moivre's Formula/Positive Integer Index

Let $z \in \C$ be a complex number expressed in polar form:
:$z = r \paren {\cos x + i \sin x}$
Then:
:$\forall n \in \Z_{>0}: \paren {r \paren {\cos x + i \sin x} }^n = r^n \paren {\map \cos {n x} + i \map \sin {n x} }$

Proof:
$\cos x + i \sin x$ is a complex number expressed in polar form $\left\langle{r, \theta}\right\rangle$ whose complex modulus is $1$ and whose argument is $x$.
From De Moivre's Formula: Positive Integer Index:
:$\forall n \in \Z_{>0}: \left({r \left({\cos x + i \sin x}\right)}\right)^n = r^n \left({\cos \left({n x}\right) + i \sin \left({n x}\right)}\right)$
The result follows by setting $r = 1$.
{{qed}}
Theorem: De Moivre's Formula/Positive Integer Index

Let $z \in \C$ be a complex number expressed in polar form:
:$z = r \paren {\cos x + i \sin x}$
Then:
:$\forall n \in \Z_{>0}: \paren {r \paren {\cos x + i \sin x} }^n = r^n \paren {\map \cos {n x} + i \map \sin {n x} }$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\cos \theta + i \sin \theta}^n
      | r = \paren {e^{i \theta} }^n
      | c = Euler's Formula
}}
{{eqn | r = e^{i n \theta}
      | c = Exponential of Product
}}
{{eqn | r = \cos n \theta + i \sin n \theta
      | c = Euler's Formula
}}
{{end-eqn}}
Theorem: De Moivre's Formula/Positive Integer Index

Let $z \in \C$ be a complex number expressed in polar form:
:$z = r \paren {\cos x + i \sin x}$
Then:
:$\forall n \in \Z_{>0}: \paren {r \paren {\cos x + i \sin x} }^n = r^n \paren {\map \cos {n x} + i \map \sin {n x} }$

Proof:
Proof by induction:
For all $n \in \Z_{> 0}$, let $\map P n$ be the proposition:
:$\paren {r \paren {\cos x + i \sin x} }^n = r^n \paren {\map \cos {n x} + i \, \map \sin {n x} }$
$\map P 1$ is the case:
:$\paren {r \paren {\cos x + i \sin x} }^1 = r^1 \paren {\map \cos {1 x} + i \, \map \sin {1 x} }$
which is trivially true.
=== Basis for the Induction ===
$\map P 2$ is the case:
:$\paren {r \paren {\cos x + i \sin x} }^2 = r^2 \paren {\map \cos {n x} + i \, \map \sin {2 x} }$
From Product of Complex Numbers in Polar Form, we have:
:$r_1 \paren {\cos x_1 + i \sin x_1 } r_2 \paren {\cos x_2 + i \sin x_2} = r_1 r_2 \paren {\map \cos {x_1 + x_2} + i \, \map \sin {x_1 + x_2} }$
Setting $r_1 = r_2 = r$ and $x_1 = x_2 = x$ gives the result.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\paren {r \paren {\cos x + i \sin x} }^k = r^k \paren {\map \cos {k x} + i \, \map \sin {k x} }$
Then we need to show:
:$\paren {r \paren {\cos x + i \sin x} }^{k + 1} = r^{k + 1} \paren {\map \cos {\paren {k + 1} x} + i \, \map \sin {\paren {k + 1} x} }$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn| l = \paren {r \paren {\cos x + i \sin x} }^{k + 1}
     | r = \paren {r \paren {\cos x + i \sin x} }^k \paren {r \paren {\cos x + i \sin x} }
}}
{{eqn| r = r^k \paren {\map \cos {k x} + i \, \map \sin {k x} } \paren {r \paren {\cos x + i \sin x} }
     | c = Induction Hypothesis
}}
{{eqn| r = r^{k + 1} \paren {\map \cos {\paren {k + 1} x} + i \, \map \sin {\paren {k + 1} x} }
     | c = Product of Complex Numbers in Polar Form
}}
{{end-eqn}}
Hence, by induction, for all $n \in \Z_{> 0}$:
:$\paren {r \paren {\cos x + i \sin x} }^n = r^n \paren {\map \cos {n x} + i \, \map \sin {n x} }$
{{qed}}
Theorem: De Moivre's Formula/Positive Integer Index

Let $z \in \C$ be a complex number expressed in polar form:
:$z = r \paren {\cos x + i \sin x}$
Then:
:$\forall n \in \Z_{>0}: \paren {r \paren {\cos x + i \sin x} }^n = r^n \paren {\map \cos {n x} + i \map \sin {n x} }$

Proof:
From Product of Complex Numbers in Polar Form: General Result:
:$z_1 z_2 \cdots z_n = r_1 r_2 \cdots r_n \paren {\map \cos {\theta_1 + \theta_2 + \cdots + \theta_n} + i \, \map \sin {\theta_1 + \theta_2 + \cdots + \theta_n} }$
Setting $z_1 = z_2 = \cdots = z_n = r \paren {\cos x + i \sin x}$ gives the result.
Theorem: De Moivre's Formula/Negative Integer Index

Let $z \in \C$ be a complex number expressed in complex form:
:$z = r \paren {\cos x + i \sin x}$
Then:
:$\forall n \in \Z_{\le 0}: \paren {r \paren {\cos x + i \sin x} }^n = r^n \paren {\map \cos {n x} + i \map \sin {n x} }$

Proof:
Let $n = 0$.
Then:
{{begin-eqn}}
{{eqn | l = r^0 \paren {\map \cos {0 x} + i \map \sin {0 x} }
      | r = 1 \times \paren {\cos 0 + i \sin 0}
      | c = {{Defof|Power (Algebra)|Zeroth Power}}
}}
{{eqn | r = 1 \paren {1 + i 0}
      | c = Cosine of Zero is One and Sine of Zero is Zero
}}
{{eqn | r = 1
      | c = 
}}
{{eqn | r = \paren {r \paren {\cos x + i \sin x} }^0
      | c = {{Defof|Power (Algebra)|Zeroth Power}}
}}
{{end-eqn}}
Now let $n \in \Z_{<0}$.
Let $n = -m$ where $m > 0$.
Thus:
{{begin-eqn}}
{{eqn | l = \paren {r \paren {\cos x + i \sin x} }^{-m}
      | r = \frac 1 {\paren {r \paren {\cos x + i \sin x} }^m}
      | c = 
}}
{{eqn | r = \frac 1 {r^m \paren {\map \cos {m x} + i \map \sin {m x} } }
      | c = De Moivre's Formula: Positive Integer Index
}}
{{eqn | r = r^{-m} \paren {\map \cos {-m x} + i \map \sin {-m x} }
      | c = {{Defof|Complex Division}}
}}
{{eqn | r = r^n \paren {\map \cos {n x} + i \map \sin {n x} }
      | c = as $n = -m$
}}
{{end-eqn}}
{{qed}}
Theorem: De Moivre's Formula/Rational Index

Let $z \in \C$ be a complex number expressed in complex form:
:$z = r \paren {\cos x + i \sin x}$
Then:
:$\forall p \in \Q: \paren {r \paren {\cos x + i \sin x} }^p = r^p \paren {\map \cos {p x} + i \, \map \sin {p x} }$

Proof:
Write $p = \dfrac a b$, where $a, b \in \Z$, $b \ne 0$.
Then:
{{begin-eqn}}
{{eqn | l = r^p \paren {\map \cos {p x} + i \, \map \sin {p x} }
      | r = \paren {r^p \paren {\map \cos {p x} + i \, \map \sin {p x} } }^{\frac b b}
}}
{{eqn | r = \paren {r^{b p} \paren {\map \cos {b p x} + i \, \map \sin {b p x} } }^{\frac 1 b}
      | c = De Moivre's Formula/Integer Index
}}
{{eqn | r = \paren {r^a \paren {\map \cos {a x} + i \, \map \sin {a x} } }^{\frac 1 b}
}}
{{eqn | r = \paren {r \paren {\cos x + i \, \sin x } }^{\frac a b}
      | c = De Moivre's Formula/Integer Index
}}
{{eqn | r = \paren {r \paren {\cos x + i \, \sin x } }^p
}}
{{end-eqn}}
{{qed}}
Theorem: Dot Product Operator is Commutative

:$\mathbf u \cdot \mathbf v = \mathbf v \cdot \mathbf u$

Proof:
{{begin-eqn}}
{{eqn | l = \mathbf u \cdot \mathbf v
      | r = \sum_{i \mathop = 1}^n u_i v_i
      | c = {{Defof|Dot Product}}
}}
{{eqn | r = \sum_{i \mathop = 1}^n v_i u_i
      | c = Real Multiplication is Commutative
}}
{{eqn | r = \mathbf v \cdot \mathbf u
      | c = {{Defof|Dot Product}}
}}
{{end-eqn}}
{{qed}}
Theorem: Dot Product Operator is Commutative

:$\mathbf u \cdot \mathbf v = \mathbf v \cdot \mathbf u$

Proof:
{{begin-eqn}}
{{eqn | l = \mathbf u \cdot \mathbf v
      | r = \norm {\mathbf u} \norm {\mathbf v} \cos \angle \mathbf u, \mathbf v
      | c = {{Defof|Dot Product|subdef = Real Euclidean Space}}
}}
{{eqn | r = \norm {\mathbf v} \norm {\mathbf u} \cos \angle \mathbf u, \mathbf v
      | c = Real Multiplication is Commutative
}}
{{eqn | r = \norm {\mathbf v} \norm {\mathbf u} \cos \angle \mathbf v, \mathbf u
      | c = Cosine Function is Even
}}
{{eqn | r = \mathbf v \cdot \mathbf u
      | c = {{Defof|Dot Product|subdef = Real Euclidean Space}}
}}
{{end-eqn}}
{{qed}}
Theorem: Dot Product with Self is Non-Negative

Let $\mathbf u$ be a vector in the real Euclidean space $\R^n$.
Then:
:$\mathbf u \cdot \mathbf u \ge 0$
where $\cdot$ denotes the dot product operator.

Proof:
{{begin-eqn}}
{{eqn | l = \mathbf u \cdot \mathbf u
      | r = \sum_{i \mathop = 1}^n {u_i}^2
      | c = {{Defof|Dot Product|subdef = General Context}}
}}
{{eqn | o = \ge
      | r = 0
      | c = as $u_i \in \R$ it follows that ${u_i}^2 \ge 0$
}}
{{end-eqn}}
{{qed}}
Theorem: Dot Product with Self is Non-Negative

Let $\mathbf u$ be a vector in the real Euclidean space $\R^n$.
Then:
:$\mathbf u \cdot \mathbf u \ge 0$
where $\cdot$ denotes the dot product operator.

Proof:
{{begin-eqn}}
{{eqn | l = \mathbf u \cdot \mathbf u
      | r = \norm {\mathbf u}^2
      | c = Dot Product of Vector with Itself
}}
{{eqn | o = \ge
      | r = 0
      | c = Square of Real Number is Non-Negative
}}
{{end-eqn}}
{{qed}}
Theorem: Dot Product with Self is Zero iff Zero Vector

:$\mathbf u \cdot \mathbf u = 0 \iff \mathbf u = \mathbf 0$

Proof:
{{begin-eqn}}
{{eqn | l = \mathbf u \cdot \mathbf u
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \sum_{i \mathop = 1}^n u_i^2
      | r = 0
      | c = {{Defof|Dot Product|subdef = General Context}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall i
      | l = u_i
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \mathbf u
      | r = \bszero
      | c = {{Defof|Zero Vector}}
}}
{{end-eqn}}
{{qed}}
Theorem: Dot Product with Self is Zero iff Zero Vector

:$\mathbf u \cdot \mathbf u = 0 \iff \mathbf u = \mathbf 0$

Proof:
Let $\mathbf u \cdot \mathbf u = 0$.
Then:
{{begin-eqn}}
{{eqn | l = 0
      | r = \norm {\mathbf u }^2 \cos \angle \mathbf u, \mathbf u
      | c = {{Defof|Dot Product|subdef = Real Euclidean Space}}
}}
{{eqn | r = \norm {\mathbf u}^2 \cos 0
      | c =
}}
{{eqn | r = \norm {\mathbf u}^2
      | c =
}}
{{end-eqn}}
The only way for this to happen is if:
:$\norm {\mathbf u} = 0$
which implies:
:$\mathbf u = \mathbf 0$
Now suppose $\mathbf u = \mathbf 0$.
Then:
{{begin-eqn}}
{{eqn | l = \mathbf u \cdot \mathbf u
      | r = \mathbf 0 \cdot \mathbf 0
      | c =
}}
{{eqn | r = \norm {\mathbf 0}^2 \cos \angle \mathbf 0, \mathbf 0
      | c =
}}
{{eqn | r = 0
      | c =
}}
{{end-eqn}}
{{qed}}
Theorem: Vector Cross Product is Anticommutative/Complex

:$\forall z_1, z_2 \in \C: z_1 \times z_2 = -\paren {z_2 \times z_1}$

Proof:
Let:
: $z_1 := x_1 + i y_1, z_2 = x_2 + i y_2$
Then:
{{begin-eqn}}
{{eqn | l = z_1 \times z_2
      | r = x_1 y_2 - y_1 x_2
      | c = {{Defof|Vector Cross Product|subdef = Complex|index = 1|Complex Cross Product}}
}}
{{eqn | r = -\paren {x_2 y_1 - y_2 x_1}
      | c = Real Addition is Commutative and Real Multiplication is Commutative
}}
{{eqn | r = -\paren {z_2 \times z_1}
      | c = {{Defof|Vector Cross Product|subdef = Complex|index = 1|Complex Cross Product}}
}}
{{end-eqn}}
{{qed}}
Theorem: Polar Form of Complex Conjugate

Let $z := r \paren {\cos \theta + i \sin \theta} \in \C$ be a complex number expressed in polar form.
Then:
:$\overline z = r \paren {\cos \theta - i \sin \theta}$
where $\overline z$ denotes the complex conjugate of $z$.

Proof:
{{begin-eqn}}
{{eqn | l = z
      | r = r \paren {\cos \theta + i \sin \theta}
      | c = 
}}
{{eqn | r = \paren {r \cos \theta} + i \paren {r \sin \theta}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \overline z
      | r = \paren {r \cos \theta} - i \paren {r \sin \theta}
      | c = {{Defof|Complex Conjugate}}
}}
{{eqn | r = r \paren {\cos \theta - i \sin \theta}
      | c = 
}}
{{end-eqn}}
{{qed}}