# Possible road-maps for proving $\lim_{x\to 0}\frac{\sin x}{x}=1$ in a non-circular way

$$\lim_{x\to 0}\frac{\sin x}{x}=1\tag{1}$$

Poofs for the limit above have been asked many many times in MSE. Here are a few of them:

Here is my question:

What are possible "road maps" for developing a proof for (1) in a non-circular rigorous way from a few axioms?

One possible "road map" is as follows:

ZFC --- natural numbers --- rational numbers --- real numbers --- limits and derivatives --- power series --- power series definition of the sine function --- proof of (1)

(In such an approach, one can derive the basic properties of the trigonometric functions from the power series definition without any appeal to the geometric notion of angle.)

[Added] My question is essential this: are there other "road maps" than the one given above?

If one is going to give an geometric argument about (1) like most introductory calculus textbooks do, then I would like to add one more question:

What axioms in geometry would you need in order to develop a satisfactory "rigorous" definition of the sine function?

• Is your question about the limit, or is your question how to define $\sin$? – GFauxPas Dec 8 '16 at 0:58
• The question about the non-circular proof of trhe limit is pretty easy to answer once you provide a rigorous definition of $\sin$. – xyzzyz Dec 8 '16 at 1:09
• I second the above comment. The missing most important detail is what definition of $\sin$ you want to consider. – Git Gud Dec 8 '16 at 1:14
• I'm not intentionally using wordplay here, but by non-circular do you mean logically it is not circular, or do you literally mean not using a circle in any of the arguments/definitions of sin? – TomGrubb Dec 19 '16 at 4:39

To make the geometric proof of (1) fully rigorous, one needs a modern rigorous treatment of Euclidean geometry, including the identification of the Euclidean plane with the Cartesian plane ${\mathbb R}^2$. This can be found in many modern Euclidean geometry texts. Euclid’s original axioms are not quite suitable for this task (Euclid being, of course, unaware of the modern framework of first-order logic and set theory), but one can use for instance Hilbert’s axioms for this purpose. Also, one eventually has to show that the geometric definition of $\sin(x)$ (from trigonometry) and the analytic definition (from power series) are equivalent. This can be done for instance by verifying that both definitions solve the same ordinary differential equation with the same initial conditions, and appealing to the Picard uniqueness theorem for such ODE; there are a number of other proofs as well (e.g. a complex analytic proof is given in these lecture notes).
• Without calculus, it comes down to the intuition that (a) circles are rectifiable i.e. the arc length can be defined, (b) circle sectors are convex, and (c) the perimeter of a convex closed curve is smaller than that of any other one strictly enclosing it. Then $\sin(x) \lt x \lt \tan(x)$ follows geometrically, see this for example. Of course, that's not formalized so it doesn't count as an answer, but I believe it could be fully formalized. – dxiv Dec 19 '16 at 18:40