avewright/proofwiki-math huggingface dataset:
Theorem: Existence of Radius of Convergence of Complex Power Series/Absolute Convergence

Let $\map {B_R} \xi$ denote the open $R$-ball of $\xi$.
Let $z \in \map {B_R} \xi$.
Then $\map S z$ converges absolutely.
If $R = +\infty$, we define $\map {B_R} \xi = \C$.

Proof:
Let $z \in \map {B_R} \xi$.
By definition of the open $R$-ball of $\xi$:
:$\cmod {z - \xi} < R$
where $\cmod z$ denotes the complex modulus of $z$.
By definition of radius of convergence, it follows that $\map S z$ converges.
Suppose $R$ is finite.
Let $\epsilon = R - \cmod {z - \xi} > 0$.
Now, let $w \in \map {B_R} \xi$ be a complex number such that $R - \cmod {w - \xi} = \dfrac \epsilon 2$.
Such a $w$ exists because, if at a loss, we can always let $w = \xi + R - \dfrac \epsilon 2$.
If $R = +\infty$, then let $w \in C$ be any complex number such that $\cmod {z - \xi} < \cmod {w - \xi}$.
Then:
{{begin-eqn}}
{{eqn | l = \limsup_{n \mathop \to \infty} \cmod {a_n \paren {z - \xi}^n}^{1/n}
      | o = <
      | r = \limsup_{n \mathop \to \infty} \cmod {a_n \paren {w - \xi}^n}^{1/n}
      | c = as $\cmod {z - \xi} < \cmod {w - \xi}$, we have $\cmod {z - \xi}^n < \cmod {w - \xi}^n$
}}
{{eqn | o = \le
      | r = 1
      | c = $n$th Root Test: $\map S w$ is not divergent
}}
{{end-eqn}}
From the $n$th Root Test, it follows that $\map S z$ converges absolutely.
{{qed}}
Theorem: Existence of Radius of Convergence of Complex Power Series/Divergence

Let $\map { {B_R}^-} \xi$ denote the closed $R$-ball of $\xi$.
Let $z \notin \map { {B_R}^-} \xi$.
Then $\map S z$ is divergent.

Proof:
Let $z \notin \map { {B_R}^-} \xi$.
Then by definition of the closed $R$-ball of $\xi$:
:$\cmod {z - \xi} > R$
where $\cmod z$ denotes the complex modulus of $z$.
By definition of radius of convergence, there exists $w \in \C$ such that:
:$\cmod {w - \xi} < \cmod {z - \xi}$
and $S \paren w$ is divergent.
Then:
{{begin-eqn}}
{{eqn | l = \limsup_{n \mathop \to \infty} \cmod {a_n \paren {z - \xi}^n}^{1/n}
      | o = >
      | r = \limsup_{n \mathop \to \infty} \cmod {a_n \paren {w - \xi}^n}^{1/n}
}}
{{eqn | o = \ge
      | r = 1
      | c = $n$th Root Test: $S \paren w$ is divergent
}}
{{end-eqn}}
From the $n$th Root Test, it follows that $\map S z$ is divergent.
{{qed}}
Theorem: Radius of Convergence of Power Series in Complex Plane

Consider the complex power series:
:$S = \ds \sum_{k \mathop = 0}^\infty z^n$
The radius of convergence $S$ is $1$.

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \dfrac {\cmod {z^n} } {\cmod {z^{n - 1} } }
      | r = \lim_{n \mathop \to \infty} \cmod {\dfrac {z^n} {z^{n - 1} } }
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \cmod z
      | c = 
}}
{{eqn | r = \cmod z
      | c = 
}}
{{end-eqn}}
By the Ratio Test, it follows that:
:$S$ is convergent for $\cmod z < 1$
:$S$ is divergent for $\cmod z > 1$.
Hence the result by definition of radius of convergence.
{{Qed}}
Theorem: Radius of Convergence of Power Series Expansion for Cosine Function

The cosine function has the complex power series expansion:
{{begin-eqn}}
{{eqn | l = \map C z
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {z^{2 n} } {\paren {2 n}!}
      | c = 
}}
{{eqn | r = 1 - \frac {z^2} {2!} + \frac {z^4} {4!} - \frac {z^6} {6!} + \cdots
      | c = 
}}
{{end-eqn}}
which is the power series expansion of the cosine function.
This is valid for all $z \in \C$.

Proof:
Applying Radius of Convergence from Limit of Sequence: Complex Case, we find that:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \cmod {\dfrac {a_{n + 1} } {a_n} }
      | r = \lim_{n \mathop \to \infty} \cmod {\dfrac {\frac {\paren {-1}^{n + 1} } {\paren {2 \paren {n + 1} }!} } {\frac {\paren {-1}^n} {\paren {2 n}!} } }
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \cmod {\dfrac {\paren {2 n}!} {\paren {2 \paren {n + 1} }!} }
      | c = as $\cmod {\paren {-1}^n} = 1$ for all $n$
}}
{{eqn | r = \lim_{n \mathop \to \infty} \cmod {\dfrac 1 {\paren {2 n + 1} \paren {2 n + 2} } }
      | c = 
}}
{{eqn | r = 0
      | c = Sequence of Powers of Reciprocals is Null Sequence
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Radius of Convergence of Power Series Expansion for Sine Function

The sine function has the complex power series expansion:
{{begin-eqn}}
{{eqn | l = S \paren z
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {z^{2 n + 1} } {\paren {2 n + 1}!}
      | c = 
}}
{{eqn | r = z - \frac {z^3} {3!} + \frac {z^5} {5!} - \frac {z^7} {7!} + \cdots
      | c = 
}}
{{end-eqn}}
which is the power series expansion of the sine function.
This is valid for all $z \in \C$.

Proof:
Applying Radius of Convergence from Limit of Sequence: Complex Case, we find that:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \cmod {\dfrac {a_{n + 1} } {a_n} }
      | r = \lim_{n \mathop \to \infty} \cmod {\dfrac {\frac {\paren {-1}^{n + 1} } {\paren {2 \paren {n + 1} + 1}!} } {\frac {\paren {-1}^n} {\paren {2 n + 1}!} } }
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \cmod {\dfrac {\paren {2 n + 1}!} {\paren {2 \paren {n + 1} + 1}!} }
      | c = as $\cmod {\paren {-1}^n} = 1$ for all $n$
}}
{{eqn | r = \lim_{n \mathop \to \infty} \cmod {\dfrac 1 {\paren {2 n + 2} \paren {2 n + 3} } }
      | c = 
}}
{{eqn | r = 0
      | c = Sequence of Powers of Reciprocals is Null Sequence
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Sum of Infinite Series of Product of nth Power of Cosine by nth Multiple of Cosine

Let $0 < \theta < \dfrac \pi 2$.
Then:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 0}^\infty \cos^n \theta \, \map \cos {n + 1} \theta
      | r = \cos \theta + \cos \theta \cos 2 \theta + \cos^2 \theta \cos 3 \theta + \cos^3 \theta \cos 4 \theta + \cdots
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}

Proof:
Let $0 < \theta < \dfrac \pi 2$.
Then $0 < \cos \theta < 1$.
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^\infty r^k \cos k \theta
      | r = \dfrac {1 - r \cos \theta} {1 - 2 r \cos \theta + r^2}
      | c = Sum of Infinite Series of Product of Power and Cosine: $\size r < 1$
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 0}^\infty \cos^k \theta \cos k \theta
      | r = \dfrac {1 - \cos^2 \theta } {1 - 2 \cos^2 \theta + \cos^2 \theta}
      | c = setting $r = \cos \theta$
}}
{{eqn | ll= \leadsto
      | l = \cos^0 \theta \cos 0 \theta + \sum_{k \mathop = 1}^\infty \cos^k \theta \cos k \theta
      | r = \dfrac {1 - \cos^2 \theta } {1 - \cos^2 \theta}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = 1 + \sum_{k \mathop = 1}^\infty \cos^k \theta \cos k \theta
      | r = \dfrac {1 - \cos^2 \theta } {1 - \cos^2 \theta}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = 1 + \sum_{k \mathop = 1}^\infty \cos^k \theta \cos k \theta
      | r = 1
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \cos \theta \sum_{k \mathop = 1}^\infty \cos^{k - 1} \theta \, \map \cos {n + 1} \theta
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 1}^\infty \cos^{k - 1} \theta \cos k \theta
      | r = 0
      | c = dividing by $\cos \theta$
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 0}^\infty \cos^k \theta \cos k \theta
      | r = 0
      | c = Translation of Index Variable of Summation
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Formula/Real Domain

Let $\theta \in \R$ be a real number.
Then:
:$e^{i \theta} = \cos \theta + i \sin \theta$

Proof:
Consider the differential equation:
:$D_z \map f z = i \cdot \map f z$
=== Step 1 ===
We will prove that $z = \cos \theta + i \sin \theta$ is a solution.
{{begin-eqn}}
{{eqn | l = z
      | r = \cos \theta + i \sin \theta
      | c = 
}}
{{eqn | l = \frac {\d z} {\d \theta}
      | r = -\sin \theta + i \cos \theta
      | c = Derivative of Sine Function, Derivative of Cosine Function, Linear Combination of Derivatives
}}
{{eqn | r = i^2 \sin \theta + i\cos \theta
      | c = $i^2 = -1$
}}
{{eqn | r = i \paren {i \sin \theta + \cos \theta}
}}
{{eqn | r = i z
}}
{{end-eqn}}
{{qed|lemma}}
=== Step 2 ===
We will prove that $y = e^{i\theta}$ is a solution.
{{begin-eqn}}
{{eqn | l = y
      | r = e^{i\theta}
      | c = 
}}
{{eqn | l = \frac {\d y} {\d \theta}
      | r = i e^{i \theta}
      | c = Derivative of Exponential Function, Chain Rule for Derivatives, Linear Combination of Derivatives
}}
{{eqn | r = i y
}}
{{end-eqn}}
{{qed|lemma}}
=== Step 3 ===
Consider the initial condition $\map f 0 = 1$.
{{begin-eqn}}
{{eqn | l = \bigvalueat y {\theta \mathop = 0}
      | r = e^{0 i}
}}
{{eqn | r = 1
}}
{{eqn | l = \bigvalueat z {\theta \mathop = 0}
      | r = \cos 0 + i \sin 0
}}
{{eqn | r = 1
}}
{{end-eqn}}
So $y$ and $z$ are both particular solutions.
But a particular solution to a differential equation is unique.
{{MissingLinks|"Specific solution" and the proof that such a specific solution is unique.}}
Therefore $y = z$, that is, $e^{i \theta} = \cos \theta + i \sin \theta$.
{{qed}}
Theorem: Euler's Formula/Real Domain

Let $\theta \in \R$ be a real number.
Then:
:$e^{i \theta} = \cos \theta + i \sin \theta$

Proof:
This:
:$e^{i \theta} = \cos \theta + i \sin \theta$
is logically equivalent to this:
:$\dfrac {\cos \theta + i \sin \theta} {e^{i \theta} } = 1$
for every $\theta$.
Note that the left expression is nowhere undefined.
Taking the derivative of this:
{{begin-eqn}}
{{eqn | l = \dfrac \d {\d \theta} e^{-i \theta} \paren {\cos \theta + i \sin \theta}
      | r = e^{-i \theta} \paren {-\sin \theta + i \cos \theta} + \paren {-i e^{-i \theta} } \paren {\cos \theta + i \sin \theta}
      | c = Product Rule for Derivatives and Derivative of Exponential Function
}}
{{eqn | r = e^{-i \theta} \paren {-\sin \theta + i \cos \theta - i \cos \theta - i^2 \sin \theta}
      | c =
}}
{{eqn | r = e^{-i \theta} \paren {-\sin \theta + i \cos \theta - i \cos \theta + \sin \theta}
      | c =
}}
{{eqn | r = e^{-i \theta} \paren 0
      | c =
}}
{{eqn | r = 0
      | c =
}}
{{end-eqn}}
Thus the expression, as a function of $\theta$, is constant and so yields the same value for every $\theta$.
We know the value at at least one point, that is, when $\theta = 0$:
:$\dfrac {\cos 0 + i \sin 0} {e^{0 i}} = \dfrac {1 + 0} 1 = 1$
Thus it is $1$ for ''every'' $\theta$, which verifies the above.
Hence the result.
{{qed}}
Theorem: Euler's Formula/Real Domain

Let $\theta \in \R$ be a real number.
Then:
:$e^{i \theta} = \cos \theta + i \sin \theta$

Proof:
Note that the following proof, as written, only holds for real $\theta$.
Define:
:$\map x \theta = e^{i \theta}$
:$\map y \theta = \cos \theta + i \sin \theta$
Consider first $\theta \ge 0$.
Taking Laplace transforms:
{{begin-eqn}}
{{eqn | l = \map {\laptrans {\map x \theta} } s
      | r = \map {\laptrans {e^{i \theta} } } s
}}
{{eqn| r = \frac 1 {s - i}
     | c = Laplace Transform of Exponential
}}
{{eqn | l = \map {\laptrans {\map y \theta} } s
      | r = \map {\laptrans {\cos \theta + i \sin \theta} } s
}}
{{eqn | r = \map {\laptrans {\cos \theta} } s + i \, \map {\laptrans {\sin \theta} } s
      | c = Linear Combination of Laplace Transforms
}}
{{eqn | r = \frac s {s^2 + 1} + \frac i {s^2 + 1}
      | c = Laplace Transform of Cosine, Laplace Transform of Sine
}}
{{eqn | r = \frac {s + i} {\paren {s + i} \paren {s - i} }
}}
{{eqn | r = \frac 1 {s - i}
}}
{{end-eqn}}
So $x$ and $y$ have the same Laplace transform for $\theta \ge 0$.
Now define $\tau = -\theta, \sigma = -s$, and consider $\theta < 0$ so that $\tau > 0$.
Taking Laplace transforms of $\map x \tau$ and $\map y \tau$: 
{{begin-eqn}}
{{eqn | l = \map {\laptrans {\map x \tau} } \sigma
      | r = \frac 1 {\sigma - i}
      | c = from above
}}
{{eqn | l = \map {\laptrans {\map y \tau} } \sigma
      | r = \frac 1 {\sigma - i}
      | c = from above
}}
{{end-eqn}}
So $\map x \theta$ and $\map y \theta$ have the same Laplace transforms for $\theta < 0$.
The result follows from Injectivity of Laplace Transform.
{{qed}}
Theorem: Euler's Formula/Real Domain

Let $\theta \in \R$ be a real number.
Then:
:$e^{i \theta} = \cos \theta + i \sin \theta$

Proof:
As Sine Function is Absolutely Convergent and Cosine Function is Absolutely Convergent, we have:
{{begin-eqn}}
{{eqn | l = \cos \theta + i \sin \theta
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \dfrac {\theta^{2 n} } {\paren {2 n}!} + i \sum_{n \mathop = 0}^\infty \paren {-1}^n \dfrac {\theta^{2 n + 1} } {\paren {2 n + 1}!}
      | c = {{Defof|Complex Cosine Function}} and {{Defof|Complex Sine Function}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {\paren {-1}^n \dfrac {\theta^{2 n} } {\paren {2 n}!} + i \paren {-1}^n \dfrac {\theta^{2 n + 1} } {\paren {2 n + 1}!} }
      | c = Sum of Absolutely Convergent Series
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {\dfrac {\paren {i \theta}^{2 n} } {\paren {2 n}!} + \dfrac {\paren {i \theta}^{2 n + 1} } {\paren {2 n + 1}!} }
      | c = {{Defof|Imaginary Unit}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \dfrac {\paren {i \theta}^n} {n!}
}}
{{eqn | r = e^{i \theta}
      | c = {{Defof|Exponential Function/Complex|subdef = Power Series Expansion|Complex Exponential Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Cosine Identity/Real Domain

:$\cos x = \dfrac {e^{i x} + e^{-i x} } 2$

Proof:
Recall the definition of the real cosine function:
{{begin-eqn}}
{{eqn | l = \cos x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n!} }
      | c = 
}}
{{eqn | r = 1 - \frac {x^2} {2!} + \frac {x^4} {4!} - \frac {x^6} {6!} + \cdots + \paren {-1}^n \frac {x^{2 n} } {\paren {2 n}!} + \cdots
      | c = 
}}
{{end-eqn}}
Recall the definition of the exponential as a power series:
{{begin-eqn}}
{{eqn | l = e^x
      | r = \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}
      | c = 
}}
{{eqn | r = 1 + x + \frac {x^2} 2 + \frac {x^3} 6 + \cdots + \frac {x^n} {n!} + \cdots
      | c = 
}}
{{end-eqn}}
Then, starting from the {{RHS}}:
{{begin-eqn}}
{{eqn | l = \frac {e^{i x} + e^{-i x} } 2
      | r = \frac 1 2 \paren {\sum_{n \mathop = 0}^\infty \frac {\paren {i x}^n} {n!} + \sum_{n \mathop = 0}^\infty \frac {\paren {-i x}^n} {n!} }
}}
{{eqn | r = \frac 1 2 \sum_{n \mathop = 0}^\infty \paren {\frac {\paren {i x}^n + \paren {-i x}^n} {n!} }
      | c = Cosine Function is Absolutely Convergent
}}
{{eqn | r = \frac 1 2 \sum_{n \mathop = 0}^\infty \paren {\frac {\paren {i x}^{2 n} + \paren {-i x}^{2 n} } {\paren {2 n}!} + \frac {\paren {i x}^{2 n + 1} + \paren {-i x}^{2 n + 1} } {\paren {2 n + 1}!} }
      | c = split into even and odd $n$
}}
{{eqn | r = \frac 1 2 \sum_{n \mathop = 0}^\infty \frac {\paren {i x}^{2 n} + \paren {-i x}^{2 n} } {\paren {2 n}!}
      | c = as $\paren {-i x}^{2 n + 1} = -\paren {i x}^{2 n + 1}$
}}
{{eqn | r = \frac 1 2 \sum_{n \mathop = 0}^\infty \frac {2 \paren {i x}^{2 n} } {\paren {2 n}!}
      | c = as $\paren {-1}^{2 n} = 1$
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {i x}^{2 n} } {\paren {2 n}!}
      | c = cancel $2$
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n}!}
      | c = as $i^{2 n} = \paren {-1}^n$
}}
{{eqn | r = \cos x
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Cosine Identity/Real Domain

:$\cos x = \dfrac {e^{i x} + e^{-i x} } 2$

Proof:
Recall Euler's Formula:
:$e^{i x} = \cos x + i \sin x$
Then, starting from the {{RHS}}:
{{begin-eqn}}
{{eqn | l = \frac {e^{i x} + e^{-i x} } 2
      | r = \frac {\cos x + i \sin x + \map \cos {-x} + i \map \sin {-x} } 2
}}
{{eqn | r = \frac {\cos x + \map \cos {-x} } 2
      | c = Sine Function is Odd
}}
{{eqn | r = \frac {2 \cos x} 2
      | c = Cosine Function is Even
}}
{{eqn | r = \cos x
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Cosine Identity/Real Domain

:$\cos x = \dfrac {e^{i x} + e^{-i x} } 2$

Proof:
{{begin-eqn}}
{{eqn | n = 1
      | l = e^{i x}
      | r = \cos x + i \sin x
      | c = Euler's Formula
}}
{{eqn | n = 2
      | l = e^{-i x}
      | r = \cos x - i \sin x
      | c = Euler's Formula: Corollary
}}
{{eqn | ll= \leadsto
      | l = e^{i x} + e^{-i x}
      | r = \paren {\cos x + i \sin x} + \paren {\cos x - i \sin x}
      | c = $(1) + (2)$
}}
{{eqn | r = 2 \cos x
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \frac {e^{i x} + e^{-i x} } 2
      | r = \cos x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Cosine Identity/Real Domain

:$\cos x = \dfrac {e^{i x} + e^{-i x} } 2$

Proof:
Consider the differential equation:
:$(1): \quad D^2_x \map f x = -\map f x$
subject to the initial conditions:
:$(2): \quad \map f 0 = 1$
:$(3): \quad D_x \map f 0 = 0$
=== Step 1 ===
We will prove that $y = \cos x$ is a particular solution of $(1)$.
{{begin-eqn}}
{{eqn | l = y
      | r = \cos x
      | c = 
}}
{{eqn | l = D^2_x y
      | r = D^2_x \cos x
      | c = taking second derivative of both sides
}}
{{eqn | r = \map {D_x} {-\sin x}
      | c = Derivative of Cosine Function
}}
{{eqn | r = -\map {D_x} {\sin x}
      | c = Derivative of Constant Multiple
}}
{{eqn | r = -\cos x
      | c = Derivative of Sine Function
}}
{{eqn | r = -y
      | c = 
}}
{{end-eqn}}
Thus $y = \cos x$ fulfils $(1)$.
Then from Cosine of Zero is One:
:$\cos 0 = 1$
Thus $y = \cos x$ fulfils $(2)$.
Then:
{{begin-eqn}}
{{eqn | l = D_x \cos 0
      | r = -\sin 0
      | c = Derivative of Cosine Function
}}
{{eqn | r = 0
      | c = Sine of Zero is Zero
}}
{{end-eqn}}
Thus $y = \cos x$ fulfils $(3)$.
So $y = \cos x$ is a particular solution of $(1)$.
{{qed|lemma}}
=== Step 2 ===
We will prove that $z = \dfrac {e^{i x} + e^{-i x} } 2$ is a particular solution of $(1)$.
{{begin-eqn}}
{{eqn | l = z
      | r = \frac {e^{i x} + e^{-i x} } 2
      | c = 
}}
{{eqn | l = D^2_x z
      | r = \map {D^2_x} {\frac {e^{i x} + e^{-i x} } 2}
      | c = taking second derivative of both sides
}}
{{eqn | r = \frac 1 2 \paren {D^2_x e^{i x} + D^2_x e^{-i x} }
      | c = Linear Combination of Derivatives
}}
{{eqn | r = \frac 1 2 \paren {i D_x e^{i x} - i D_x e^{-i x} }
      | c = Derivative of Exponential Function
}}
{{eqn | r = \frac 1 2 \paren {i^2 e^{i x} - i \paren {-i} e^{-i x} }
      | c = Derivative of Exponential Function
}}
{{eqn | r = \frac 1 2 \paren {- e^{i x} - e^{-i x} }
      | c = $i^2 = -1$
}}
{{eqn | r = -\frac {e^{i x} + e^{-i x} }2
      | c = 
}}
{{eqn | r = -z
      | c = 
}}
{{end-eqn}}
Thus $z = \dfrac {e^{i x} + e^{-i x} } 2$ fulfils $(1)$.
Then:
{{begin-eqn}}
{{eqn | l = \frac {e^{i \times 0} + e^{-i \times 0} } 2
      | r = \frac {1 + 1} 2
      | c = Exponential of Zero
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
Thus $z = \dfrac {e^{i x} + e^{-i x} } 2$ fulfils $(2)$.
Then:
{{begin-eqn}}
{{eqn | l = \intlimits {D_x \frac {e^{i x} + e^{-i x} } 2} {x \mathop = 0} {}
      | r = \intlimits {\frac {i e^{i x} - i e^{-i x} } 2} {x \mathop = 0} {}
      | c = Derivative of Exponential Function
}}
{{eqn | r = \frac {i - i} 2
      | c = Exponential of Zero
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
Thus $z = \dfrac {e^{i x} + e^{-i x} } 2$ fulfils $(3)$.
So $z = \dfrac {e^{i x} + e^{-i x} } 2$ is a particular solution of $(1)$.
{{qed|lemma}}
We have shown that $y$ and $z$ are both particular solutions of $(1)$.
But a particular solution to a differential equation is unique.
{{MissingLinks|This result definitely needs backing up with an appropriate link}}
Therefore $y = z$.
That is:
:$\cos x = \dfrac {e^{i x} + e^{-i x} } 2$
{{qed}}
Theorem: Euler's Sine Identity/Real Domain

:$\sin x = \dfrac {e^{i x} - e^{-i x} } {2 i}$

Proof:
Recall the definition of the sine function:
{{begin-eqn}}
{{eqn | l = \sin x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!}
      | c = 
}}
{{eqn | r = x - \frac {x^3} {3!} + \frac {x^5} {5!} - \frac {x^7} {7!} + \cdots + \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!} + \cdots
      | c = 
}}
{{end-eqn}}
Recall the definition of the exponential as a power series:
{{begin-eqn}}
{{eqn | l = e^x
      | r = \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}
      | c = 
}}
{{eqn | r = 1 + \frac x {1!} + \frac {x^2} {2!} + \frac {x^3} {3!} + \cdots + \frac {x^n} {n!} + \cdots
      | c = 
}}
{{end-eqn}}
Then, starting from the {{RHS}}:
{{begin-eqn}}
{{eqn | l = \frac {e^{i x} - e^{-i x} } {2 i}
      | r = \frac 1 {2 i} \paren {\sum_{n \mathop = 0}^\infty \frac {\paren {i x}^n} {n!} - \sum_{n \mathop = 0}^\infty \frac {\paren {-i x}^n} {n!} }
      | c = 
}}
{{eqn | r = \frac 1 {2 i} \sum_{n \mathop = 0}^\infty \paren {\frac {\paren {i x}^n - \paren {-i x}^n} {n!} }
      | c = 
}}
{{eqn | r = \frac 1 {2 i} \sum_{n \mathop = 0}^\infty \paren {\frac {\paren {i x}^{2 n} - \paren {-i x}^{2 n} } {\paren {2 n}!} + \frac {\paren {i x}^{2 n + 1} - \paren {-i x}^{2 n + 1} } {\paren {2 n + 1}!} }
      | c = split into even and odd $n$
}}
{{eqn | r = \frac 1 {2 i} \sum_{n \mathop = 0}^\infty \frac {\paren {i x}^{2 n + 1} - \paren {-i x}^{2 n + 1} } {\paren {2 n + 1}!}
      | c = as $\paren {-i x}^{2 n} = \paren {i x}^{2 n}$
}}
{{eqn | r = \frac 1 {2 i} \sum_{n \mathop = 0}^\infty \frac {2 \paren {i x}^{2 n + 1} } {\paren {2 n + 1}!}
      | c = as $\paren {-1}^{2 n + 1} = -1$
}}
{{eqn | r = \frac 1 i \sum_{n \mathop = 0}^\infty \frac {\paren {i x}^{2 n + 1} } {\paren {2 n + 1}!}
      | c = cancel $2$
}}
{{eqn | r = \frac 1 i \sum_{n \mathop = 0}^\infty \frac {i \paren {-1}^n x^{2 n + 1} } {\paren {2 n + 1}!}
      | c = as $i^{2 n + 1} = i \paren {-1})^n $
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1!} }
      | c = cancel $i$
}}
{{eqn | r = \sin x
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Sine Identity/Real Domain

:$\sin x = \dfrac {e^{i x} - e^{-i x} } {2 i}$

Proof:
Recall Euler's Formula:
:$e^{i x} = \cos x + i \sin x$
Then, starting from the {{RHS}}:
{{begin-eqn}}
{{eqn | l = \frac {e^{i x} - e^{-i x} }{2 i}
      | r = \frac {\paren {\cos x + i \sin x} - \paren {\map \cos {-x} + i \map \sin {-x} } } {2 i}
}}
{{eqn | r = \frac {\paren {\cos x + i \sin x - \cos x - i \map \sin {-x} } } {2 i}
      | c = Cosine Function is Even
}}
{{eqn | r = \frac {i \sin x - i \map \sin {-x} } {2 i}
      | c = 
}}
{{eqn | r = \frac {i \sin x - i \paren {-\map \sin {-x} } } {2 i}
      | c = Sine Function is Odd
}}
{{eqn | r = \frac {2 i \sin x} {2 i}
      | c = 
}}
{{eqn | r = \sin x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Sine Identity/Real Domain

:$\sin x = \dfrac {e^{i x} - e^{-i x} } {2 i}$

Proof:
{{begin-eqn}}
{{eqn | n = 1
      | l = e^{i x}
      | r = \cos x + i \sin x
      | c = Euler's Formula
}}
{{eqn | n = 2
      | l = e^{-i x}
      | r = \cos x - i \sin x
      | c = Euler's Formula: Corollary
}}
{{eqn | ll= \leadsto
      | l = e^{i x} - e^{-i x}
      | r = \paren {\cos x + i \sin x} - \paren {\cos x - i \sin x}
      | c = $(1) - (2)$
}}
{{eqn | r = 2 i \sin x
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \frac {e^{i x} - e^{-i x} } {2 i}
      | r = \sin x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Reverse Triangle Inequality/Normed Division Ring

Let $\struct {R, \norm {\,\cdot\,} }$ be a normed division ring.
Then:
:$\forall x, y \in R: \norm {x - y} \ge \bigsize {\norm x - \norm y}$

Proof:
Let $0$ be the zero of $\struct {R, \norm {\,\cdot\,} }$.
Let $d$ denote the metric induced by $\norm {\, \cdot \,}$, that is:
:$\map d {x, y} = \norm {x - y}$
From Metric Induced by Norm on Normed Division Ring is Metric we have that $d$ is indeed a metric.
Then, from the Reverse Triangle Inequality as applied to metric spaces:
:$\forall x, y, z \in R: \bigsize {\norm {x - z} - \norm {y - z} } \le \norm {x - y}$
Then:
:$\forall x, y \in R: \bigsize {\norm x - \norm y} = \bigsize {\norm{x - 0} - \norm{y - 0} } \le \norm {x - y}$
{{qed}}
Category:Triangle Inequality
Category:Normed Division Rings
s4owpzx2q00sisb93nn4yho7dlsvgj2