Solve Limit Tend To $\pi$, From Length Of Circle Computing the length of a semicircle of radius 1. It's divided in $2^x$ equal arcs, I find the following formula for the total length of the chords created:
$$L=2^{x+1} \sin \left( \frac{45}{2^{x-1}} \right)$$
When $x \to \infty$ we see, geometrically, that this expression tends to be  the length of the circle:
$$2^{x+1} \sin \left( \frac{45}{2^{x-1}} \right)$$
My goal is to define $\pi$ as the value of that expression when $x \to \infty$ (the limit). But how can I rigorously prove that this limit exists and that the expression tends to be the length of the circle? In other words, how can I write rigorously the geometric ideas?
Note: The number  $\frac{45}{2^{x-1}}$ is in degrees.
 A: Well, if you define $45^{\circ}$ as equal to $\displaystyle\frac{\pi}{4}$ radians (equivalent to defining $\pi$ by $\text{circumference} = \pi d$), the limit's existence and value follows:
$$\lim_{n\to\infty}2^{n+1}\sin\bigg(\frac{45^{\circ}}{2^{n-1}}\bigg)=\lim_{n\to\infty}2^{n+1}\sin\bigg(\frac{\pi}{4\cdot2^{n-1}}\bigg)=\lim_{n\to\infty}\pi\cdot\frac{\displaystyle\sin\big(\frac{\pi}{2^{n+1}}\big)}{\displaystyle\frac{\pi}{2^{n+1}}}$$
$$=\pi\lim_{\frac{\pi}{2^{n+1}}\to 0^{+}}\frac{\displaystyle\sin\big(\frac{\pi}{2^{n+1}}\big)}{\displaystyle\frac{\pi}{2^{n+1}}}=\boxed{\pi}$$
A: Converted to radians, we have
$$L_x=2^{x+1} \sin \left(\frac{\pi }{2^{x+1}}\right)$$ Use the double inequality
$$t-\frac{t^3}{6} \leq \sin(t) \leq t$$ which makes
$$\pi -\frac{\pi ^3}{24 \times 4^x}\leq L_x \leq \pi$$ So, if you need $k$ significant figures
$$x_{(k)}= -\frac{\log \left(\frac{3\ 10^{-k}}{\pi ^2}\right)}{2 \log (2)}-\frac{3}{2}$$ For $k=10$, then $x=16$ and computing
$$L_{16}=131072 \sin \left(\frac{\pi }{131072}\right)=\color{red}{3.141592653}29$$
