Theorem: Euler Formula for Sine Function/Complex Numbers

{{begin-eqn}}
{{eqn | l = \sin z
      | r = z \prod_{n \mathop = 1}^\infty \paren {1 - \frac {z^2} {n^2 \pi^2} }
      | c = 
}}
{{eqn | r = z \paren {1 - \dfrac {z^2} {\pi^2} } \paren {1 - \dfrac {z^2} {4 \pi^2} } \paren {1 - \dfrac {z^2} {9 \pi^2} } \dotsm
      | c = 
}}
{{end-eqn}}
for all $z \in \C$.

Proof:
For $z \in \C$ and $n \in \N$, let:
:$\ds \map {I_n} z = \int_0^{\pi / 2} \cos {z t} \cos^n t \rd t $
Observe that $\map {I_0} 0 = \dfrac {\pi} 2$ and:
{{begin-eqn}}
{{eqn | l = \map {I_0} z
      | r = \int_0^{\pi / 2} \cos {z t} \rd t
      | c = 
}}
{{eqn | r = \frac 1 z \map \sin {\frac {\pi z} 2}
      | c = 
}}
{{end-eqn}}
which yields:
:$(1): \quad \map \sin {\dfrac {\pi z} 2} = \dfrac {\pi z} 2 \dfrac {\map {I_0} z} {\map {I_0} 0}$
Integrating by parts twice with $n \ge 2$, we have:
{{begin-eqn}}
{{eqn | l = z \map {I_n} z
      | r = n \int_0^{\pi / 2} \sin {z t} \cos^{n - 1} t \sin t \rd t 
      | c = 
}}
{{eqn | l = z^2 \map {I_n} z
      | r = n \int_0^{\pi / 2} \cos {z t} \paren {\cos^n t - \paren {n - 1} \cos^{n - 2} t \sin^2 t} \rd t
      | c = 
}}
{{eqn | r = n \int_0^{\pi / 2} \cos {z t} \paren {n \cos^n t - \paren {n - 1} \cos^{n - 2} t } \rd t
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = n^2 \map {I_n} z - n \paren {n - 1} \map {I_{n - 2} } z
      | c = 
}}
{{end-eqn}}
which yields the reduction formula:
:$n \paren {n - 1} \map {I_{n - 2} } z = \paren {n^2 - z^2} \map {I_n} z$
Substituting $z = 0$ we obtain:
:$n \paren {n - 1} \map {I_{n - 2} } 0 = n^2 \map {I_n} 0$
From Shape of Cosine Function, it is clear that $\map {I_n} 0 > 0$ for $n \ge 0 $.
Therefore we can divide the two equations to get:
:$(2): \quad \dfrac {\map {I_{n - 2} } z} {\map {I_{n - 2} } 0} = \paren {1 - \dfrac {z^2} {n^2} } \dfrac {\map {I_n} z} {\map {I_n} 0}$
We have:
{{begin-eqn}}
{{eqn | l = \cmod {1 - \cos {z t} }
      | r = \cmod {1 - \map \cos {x + i y} t}
      | c = 
}}
{{eqn | r = \cmod {1 - \cos {x t} \cos {i y t} + \sin x t \sin {i y t} }
      | c = Cosine of Sum
}}
{{eqn | r = \cmod {1 - \cos {x t} \cosh {y t} + i \sin {x t} \sinh {y t} }
      | c = Hyperbolic Sine in terms of Sine and Hyperbolic Cosine in terms of Cosine
}}
{{eqn | r = \sqrt {\paren {1 - \cos {x t} \cosh {y t} }^2 + \paren {\sin {x t} \sinh {y t} }^2}
      | c = 
}}
{{eqn | r = \sqrt {4 \map {\sinh^4} {\frac {y t} 2} + 8 \map {\sinh^2} {\frac {y t} 2} \map {\sin^2} {\frac {x t} 2} + 4 \map {\sin^4} {\frac {x t} 2} }
      | c = Double Angle Formulas
}}
{{eqn | r = 2 \map {\sinh^2} {\frac {y t} 2} + 2 \sin^2 {\frac {x t} 2}
      | c = 
}}
{{end-eqn}}
From Sine Inequality we have that $2 \map {\sin^2} {\dfrac {x t} 2} \le \dfrac 1 2 x^2 t^2$.
By Lemma 1, $\dfrac {\sinh x} x$ is an increasing function for $x \ge 0$, so for $t \in \closedint 0 {\dfrac {\pi} 2}$:
{{begin-eqn}}
{{eqn | o = \le
      | l = \frac {\map \sinh {y t / 2} } {y t / 2}
      | r = \frac {\map \sinh {y \pi / 4} } {y \pi /  4}
      | c = 
}}
{{eqn | ll= \leadsto
      | o = \le
      | l = \frac {\map {\sinh^2} {y t / 2} } {\paren {y t / 2}^2}
      | r = \frac {\map {\sinh^2} {y \pi / 4} } {\paren {y \pi / 4}^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | o = \le
      | l = 2 \map {\sinh^2} {y t / 2}
      | r = \frac 1 2 \frac {\map {\sinh^2} {y \pi / 4} } {\paren {y \pi / 4}^2} t^2
      | c =
}}
{{end-eqn}}
So we deduce:
{{begin-eqn}}
{{eqn | o = \le
      | l = \cmod {1 - \cos {z t} }
      | r = \frac 1 2 \paren {x^2 + \frac {\map {\sinh^2} {y \pi / 4} } {\paren {\pi / 4}^2} } t^2
      | c = 
}}
{{eqn | r = \map C {x, y} t^2
      | c = where $C$ is a non-negative function of $x$ and $y$ 
}}
{{end-eqn}}
By Relative Sizes of Definite Integrals we have:
{{begin-eqn}}
{{eqn | l = \cmod {\map {I_n} 0 - \map {I_n} z}
      | r = \cmod {\int_0^{\pi / 2} \paren {1 - \cos {z t} } \cos^n t \rd t}
      | c = 
}}
{{eqn | o = \le
      | r = \map C {x, y} \int_0^{\pi / 2} t^2 \cos^n t \rd t
      | c = Cosine Inequality
}}
{{eqn | o = \le
      | r = \map C {x, y} \int_0^{\pi / 2} t \cos^{n - 1} t \sin t \rd t
      | c = Tangent Inequality
}}
{{eqn | r = \frac {\map C {x, y} } n \int_0^{\pi / 2} \cos^n t \rd t
      | c = Integration by Parts
}}
{{eqn | r = \frac {\map C {x, y} } n \map {I_n} 0
      | c = 
}}
{{end-eqn}}
which yields the inequality:
:$\cmod {1 - \dfrac {\map {I_n} z} {\map {I_n} 0} } \le \dfrac {\map C {x, y} } n$
It follows from Squeeze Theorem that:
:$(3): \quad \ds \lim_{n \mathop \to \infty} \frac {\map {I_n} z} {\map {I_n} 0} = 1$
Consider the equation, for even $n$:
:$\ds \map \sin {\dfrac {\pi z} 2} = \dfrac {\pi z} 2 \prod_{i \mathop = 1}^{n / 2} \paren {1 - \dfrac {z^2} {\paren {2 i}^2} } \dfrac {\map {I_n} z} {\map {I_n} 0}$
This is true for $n = 0$ by $(1)$.
Suppose it is true for some $n = k$.
Then:
{{begin-eqn}}
{{eqn | l = \map \sin {\frac {\pi z} 2}
      | r = \frac {\pi z} 2 \prod_{i \mathop = 1}^{k / 2} \paren {1 - \frac {z^2} {\paren {2 i}^2} } \frac {\map {I_k} z} {\map {I_k} 0}
      | c = 
}}
{{eqn | r = \frac {\pi z} 2 \prod_{i \mathop = 1}^{\paren {k + 2} / 2} \paren {1 - \frac {z^2} {\paren {2 i}^2} } \frac {\map {I_{k + 2} } z} {\map {I_{k + 2} } 0}
      | c = by $(2)$
}}
{{end-eqn}}
So it is true for all even $n$ by induction.
Taking the limit as $n \to \infty$ we have:
{{begin-eqn}}
{{eqn | l = \map \sin {\frac {\pi z} 2}
      | r = \lim_{n \mathop \to \infty} \frac {\pi z} 2 \prod_{i \mathop = 1}^{n / 2} \paren {1 - \frac {z^2} {\paren {2 i}^2} } \frac {\map {I_n} z} {\map {I_n} 0}
      | c = 
}}
{{eqn | r = \frac {\pi z} 2 \prod_{i \mathop = 1}^\infty \paren {1 - \frac {z^2} {\paren {2 i}^2} } \lim_{n \mathop \to \infty} \frac {\map {I_n} z} {\map {I_n} 0}
      | c = Product Rule for Limits of Complex Functions
}}
{{eqn | r = \frac {\pi z} 2 \prod_{i \mathop = 1}^\infty \paren {1 - \frac {z^2} {\paren {2 i}^2} }
      | c = by $(3)$
}}
{{end-eqn}}
or equivalently, letting $\dfrac {\pi z} 2 \mapsto z$:
:$\ds \sin z = z \prod_{n \mathop = 1}^\infty \paren {1 - \frac {z^2} {n^2 \pi^2} }$
{{qed}}