Prove this formula for the $\sin\left(\frac{x}{2^n}\right), x \in [0,\frac{\pi}{2}[, n \in \Bbb{N}$ The formula in question:
$$\sin\left(\frac{x}{2^n}\right) = \sqrt{a_1-\sqrt{a_2+\sqrt{a_3+\sqrt{a_4+\dots+\sqrt{a_{n-1}+\sqrt{\frac{a_{n-1}}{2}\left(1-\sin^2(x)\right)}}}}}}$$
where
$$a_k = \frac{1}{2^{2^k-1}} \quad \forall k \in \{1,2,\dots,n-1\}, \ n \in \Bbb{N}, \ x \in \left[0,\frac{\pi}{2}\right[$$
and only the first sign (after $a_1$) is $-$, the rest is $+$.
If this holds, this is a great way to calculate the $\sin$ of small angles, specifically ones that are a power of $\frac{1}{2}$ radians.
My attempt:
I have derived at this by continously using the formula
$$\sin\left(\frac{x}{2}\right) = \sqrt{\frac{1-\sqrt{1-\sin^2(x)}}{2}} = \sqrt{\frac{1}{2}-\sqrt{\frac{1}{4}-\frac{\sin^2(x)}{4}}}$$
Which holds true, since
$$
\begin{align}
\sin(2x) &= 2\sin(x)\cos(x) \\
\sin(x) &= 2\sin\left(\frac{x}{2}\right)\cos\left(\frac{x}{2}\right) \\
\sin(x) &= 2\sin\left(\frac{x}{2}\right)\sqrt{1-\sin^2\left(\frac{x}{2}\right)} \\
\sin^2(x) &= 4\sin^2\left(\frac{x}{2}\right)\left(1-\sin^2\left(\frac{x}{2}\right)\right) \ \left(\text{if } x \in \left[0,\frac{\pi}{2}\right[\right) \\
\sin^2(x) &= 4\sin^2\left(\frac{x}{2}\right)-4\sin^4\left(\frac{x}{2}\right) \\
0 &= 4\sin^4\left(\frac{x}{2}\right)-4\sin^2\left(\frac{x}{2}\right)+\sin^2(x) \\
\sin^2\left(\frac{x}{2}\right)_{1,2} &= \frac{4 \pm \sqrt{16-16\sin^2(x)}}{8} = \frac{1 \pm \sqrt{1-\sin^2(x)}}{2}
\end{align}
$$
And this holds true with $-$, since:
$$
\begin{align}
\sin^2\left(\frac{x}{2}\right) &\stackrel{?}{=} \frac{1-\sqrt{1-\sin^2(x)}}{2} \\
2\sin^2\left(\frac{x}{2}\right) &\stackrel{?}{=} 1-\cos(x) \\
2\sin^2\left(\frac{x}{2}\right) &\stackrel{?}{=} 1-\cos^2\left(\frac{x}{2}\right)+\sin^2\left(\frac{x}{2}\right) \\
\sin^2\left(\frac{x}{2}\right) &\stackrel{?}{=} 1-\cos^2\left(\frac{x}{2}\right)
\end{align}
$$
Yes, since
$$
\sin^2\left(\frac{x}{2}\right) + \cos^2\left(\frac{x}{2}\right) = 1
$$
So we found that if $x \in \left[0,\frac{\pi}{2}\right[$, then
$$\sin\left(\frac{x}{2}\right) = \sqrt{\frac{1-\sqrt{1-\sin^2(x)}}{2}}$$
Now I plugged the formula into itself a couple times, and guessed what it would look like if I had plugged it in $n$ times. However, I have only assumed the above values of $a_k$ are true by looking at the results, so I'd like a rigorous proof of the formula.
I tried induction by $n$, but I couldn't figure out the $n \rightarrow n+1$ step.
Question:
Provide a proof of the first formula or correct it if it's wrong.
 A: It's a bit tedious, but nonetheless doable:
Since we have
\begin{align}\sin\left(\frac{x}{{2^{n+1}}}\right)&= \sqrt{\frac{1}{2}-\sqrt{\frac{1}{4}-\frac{\sin^2\left(\frac{x}{{2^{n}}}\right)}{4}}}
\end{align}
We can use the induction hypothesis to calculate
\begin{align*}\frac{1}{4}\cdot\sin^2\left(\frac{x}{{2^{n}}}\right)&=\frac{1}{4}\cdot \left(a_1-\sqrt{a_2+\sqrt{a_3+\sqrt{a_4+\dots+\sqrt{a_{n-1}+\sqrt{\frac{a_{n-1}}{2}\left(1-\sin^2(x)\right)}}}}}\right)\\
&=\frac{a_1}{2^2}-\sqrt{\frac{a_2}{(2^{2})^2}+\sqrt{\frac{a_3}{((2^{2})^2)^2}+\sqrt{\frac{a_4}{2^{2^4}}+\dots+\sqrt{\frac{a_{n-1}}{2^{2^{n-1}}}+\sqrt{\frac{a_{n}}{2^{2^n}\cdot 2}\left(1-\sin^2(x)\right)}}}}}\\
&=a_2-\sqrt{a_3+\sqrt{a_4+\sqrt{a_5+\dots+\sqrt{a_{n}+\sqrt{\frac{a_{n+1}}{2}\left(1-\sin^2(x)\right)}}}}}
\end{align*}
where we used that
$$\frac{a_n}{2^{2^n}}=\frac{1}{2^{2^n-1}\cdot 2^{2^n}}=\frac{1}{2^{2\cdot 2^{n}-1}}=\frac{1}{2^{2^{n+1}-1}}=a_{n+1}$$
And since
$$\color{red}{a_1=\frac{1}{2^{2^1-1}}=\frac{1}{2}}$$
and $a_2=\frac{1}{2^{2^2-1}}=\frac{1}{8}$ so that 
$$\color{blue}{\frac{1}{4}-a_2=\frac{1}{4}-\frac{1}{8}=\frac{1}{8}=a_2}$$
you get
\begin{align}\sin\left(\frac{x}{{2^{n+1}}}\right)&= \sqrt{\frac{1}{2}-\sqrt{\frac{1}{4}-\frac{\sin^2\left(\frac{x}{{2^{n}}}\right)}{4}}}\\
&= \sqrt{\color{red}{\frac{1}{2}}-\sqrt{\color{blue}{\frac{1}{4}-a_2}+\sqrt{a_3+\sqrt{a_4+\sqrt{a_5+\dots+\sqrt{a_{n}+\sqrt{\frac{a_{n+1}}{2}\left(1-\sin^2(x)\right)}}}}}}}\\
&= \sqrt{\color{red}{a_1}-\sqrt{\color{blue}{a_2}+\sqrt{a_3+\sqrt{a_4+\sqrt{a_5+\dots+\sqrt{a_{n}+\sqrt{\frac{a_{n+1}}{2}\left(1-\sin^2(x)\right)}}}}}}}
\end{align}
