Theorem: Euler Formula for Sine Function/Real Numbers

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

Proof:
For $x \in \R$ and $n \in \N_{> 0}$, let:
:$\map {f_n} x = \dfrac 1 2 \paren {\paren {1 + \dfrac x n}^n - \paren {1 - \dfrac x n}^n }$
Then $\map {f_n} x = 0$ {{iff}}:
{{begin-eqn}}
{{eqn | l = \paren {1 + \frac x n}^n
      | r = \paren {1 - \frac x n}^n
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = 1 + \frac x n 
      | r = \paren {1 - \frac x n} e^{2 \pi i \frac k n}
      | c = for $k \in \Z$
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = n \frac {e^{2 \pi i \frac k n} - 1} {e^{2 \pi i \frac k n} + 1}
      | c = 
}}
{{eqn | r = n i \, \map \tan {\frac {k \pi} n }
      | c = Euler's Tangent Identity
}}
{{end-eqn}}
Hence the roots of $\map {f_{2 m + 1} } x$ are:
:$\paren {2 m + 1} i \, \map \tan {\dfrac {k \pi} {2 m + 1} }$ 
for $-m \le k \le m$.
Observe that $\map {f_{2 m + 1} } x$ is a polynomial of degree $2 m + 1$. 
Then for some constant $C$, we have:
{{begin-eqn}}
{{eqn | l = \map {f_{2 m + 1} } x
      | r = C x \prod_{\substack {k \mathop = - m \\ k \mathop \ne 0} }^m \paren {1 - \frac x {\paren {2 m + 1} i \, \map \tan {k \pi / \paren {2 m + 1} } } }
      | c = Polynomial Factor Theorem
}}
{{eqn | r = C x \prod_{k \mathop = 1}^m \paren {1 + \frac {x^2} {\paren {2 m + 1}^2 \map {\tan^2} {k \pi / \paren {2 m + 1} } } }
      | c = Tangent Function is Odd
}}
{{end-eqn}}
It can be seen from Binomial Theorem for Integral Index that the coefficient of $x$ in $\map {f_{2 m + 1} } x$ is $1$.
Hence $C = 1$, and we obtain:
:$\ds \map {f_{2 m + 1} } x = x \prod_{k \mathop = 1}^m \paren {1 + \frac {x^2} {\paren {2 m + 1}^2 \map {\tan^2} {k \pi / \paren {2 m + 1} } } }$
Let $l < m$.
Then:
:$\ds x \prod_{k \mathop = 1}^l \paren {1 + \frac {x^2} {\paren {2 m + 1}^2 \map {\tan^2} {k \pi / \paren {2 m + 1} } } } \le \map {f_{2 m + 1} } x$
Taking the limit as $m \to \infty$ we have:
{{begin-eqn}}
{{eqn | l = \lim_{m \mathop \to \infty} x \prod_{k \mathop = 1}^l \paren {1 + \frac {x^2} {k^2 \pi^2} \paren {\frac {k \pi / \paren {2 m + 1} } {\map \tan {k \pi / \paren {2 m + 1} } } }^2 }
      | o = \le 
      | r = \frac 1 2 \paren {e^x - e^{-x} }
      | c = {{Defof|Exponential Function/Real|subdef = Limit of Sequence|Exponential Function}}
}}
{{eqn | ll= \leadsto
      | o = \le
      | l = x \prod_{k \mathop = 1}^l \paren {1 + \frac {x^2} {k^2 \pi^2} }
      | r = \sinh x
      | c = Limit of $\dfrac {\tan x} x$ at Zero and {{Defof|Hyperbolic Sine}}
}}
{{end-eqn}}
By Tangent Inequality, we have:
:$\map \tan {\dfrac {k \pi} {2 m + 1} } \ge \dfrac {k \pi} {2 m + 1}$
and hence:
:$\ds \map {f_{2 l + 1} } x \le x \prod_{k \mathop = 1}^l \paren {1 + \frac {x^2} {k^2 \pi^2} } \le \sinh x$
Taking the limit as $l \to \infty$, we have by the Squeeze Theorem:
:$\ds x \prod_{k \mathop = 1}^\infty \paren {1 + \frac {x^2} {k^2 \pi^2} } = \sinh x$
Substituting $x \mapsto i x$, we obtain:
:$\ds \sin x = x \prod_{k \mathop = 1}^\infty \paren {1 - \frac {x^2} {k^2 \pi^2} }$
{{qed}}