This answer shows using only elementary geometry that $\sin \alpha / \sin \beta < \alpha / \beta$ for all commensurable angles $\beta < \alpha$ in the first quadrant, and hence (extending to all angles) that $(a_n)$ (in your own answer above) is strictly increasing. A question related to yours is here where we find only a tiny amount of analysis is needed to formally define $\pi$ within geometry. The sequence $(p_n)$ considered there is essentially the same as the $(a_n)$ you consider here. Formally defining radian measure is not trivial, but we need that to prove rigorously that the purely geometric trig functions (and $\pi$) are 'isomorphically' identical to their analytically defined counterparts. We also need to differentiate angles in geometry from real numbers, and to formally define the concept of 'angle measure' within geometry which links the two - the essential property is 'additivity'.

This answer to Geometrically showing $\frac{\alpha}{\beta} > \frac{\sin\alpha}{\sin\beta}$, for $0 < \beta < \alpha < 90^\circ$ shows using only elementary geometry that $\sin \alpha / \sin \beta < \alpha / \beta$ for all commensurable angles $\beta < \alpha$ in the first quadrant, and hence (extending to all angles) that $(a_n)$ (in your own answer above) is strictly increasing. A question related to yours is Can The Existence Of $\pi$ Be Proved Without Formal Analysis? where we find only a tiny amount of analysis is needed to formally define $\pi$ within geometry. The sequence $(p_n)$ considered there is essentially the same as the $(a_n)$ you consider here. Formally defining radian measure is not trivial, but we need that to prove rigorously that the purely geometric trig functions (and $\pi$) are 'isomorphically' identical to their analytically defined counterparts. We also need to differentiate angles in geometry from real numbers, and to formally define the concept of 'angle measure' within geometry which links the two — the essential property is 'additivity'.

This answer shows using only elementary geometry that $\sin \alpha / \sin \beta < \alpha / \beta$ for all commensurable angles $\beta < \alpha$ in the first quadrant, and hence (extending to all angles) that $(a_n)$ (in your own answer above) is strictly increasing. A question related to yours is here where we find only a tiny amount of analysis is needed to formally define $\pi$ within geometry. The sequence $(p_n)$ considered there is essentially the same as the $(a_n)$ you consider here. Formally defining radian measure is not trivial, but we need that to prove rigorously that the purely geometric trig functions (and $\pi$) are 'isomorphically' identical to the analytically defined ones. We also need to differentiate angles in geometry from real numbers, and to formally define the concept of 'angle measure' within geometry which links the two - the essential property is 'additivity'.

This answer shows using only elementary geometry that $\sin \alpha / \sin \beta < \alpha / \beta$ for all commensurable angles $\beta < \alpha$ in the first quadrant, and hence (extending to all angles) that $(a_n)$ (in your own answer above) is strictly increasing. A question related to yours is here where we find only a tiny amount of analysis is needed to formally define $\pi$ within geometry. The sequence $(p_n)$ considered there is essentially the same as the $(a_n)$ you consider here. Formally defining radian measure is not trivial, but we need that to prove rigorously that the purely geometric trig functions (and $\pi$) are 'isomorphically' identical to their analytically defined counterparts. We also need to differentiate angles in geometry from real numbers, and to formally define the concept of 'angle measure' within geometry which links the two - the essential property is 'additivity'.