Axiomatic construction of trigonometric functions I am able to construct functions $\sin,\cos\colon \mathbb R \to \mathbb R$ satisfying the following properties:

*

*$\sin^2 x + \cos^2 x = 1$,

*$\sin(x+y)=\sin x \cos y + \sin y\cos x$, $\cos(x+y)=\cos x \cos y - \sin x \sin y$,

*$\sin(0)=0$, $\cos(0)=1$

*there exists $\tau>0$ such that $\sin$ and $\cos$ are $\tau$-periodic

*$\sin$ is strictly increasing if restricted to $[-\tau/4,\tau/4]$.

If you prefer, last condition can also be replaced with


*$\sin$ and $\cos$ are continuous.

How can I prove that $\lim_{x\to 0} \frac{\sin x}{x}$ exists and is finite?
I'm trying to define the trigonometric functions following the geometric intuition so I cannot assume that the trigonometric function have been defined and cannot use the complex exponential. I also don't want to use integrals or differential equations.
The above functions are obtained by choosing some unit to measure angles and following the geometric definition of trigonometric functions. If we replace $\sin x$ and $\cos x$ with $\sin cx$ and $\cos cx$ for any $c>0$ we obtain another pair of trigonometric functions with the same properties as above and period $\tau/c$ in place of $\tau$.
The above construction can be achieved by using the natural isomorphism between totally ordered, dense, continuous, additive groups in exactly the same way which allows us to define an isomorphism between the additive group of real numbers and the multiplicative group of positive real numbers obtaining the exponential function $a^x$ for any positive $a$. In fact we can restate the trigonometric functions as real and imaginary part of a complex function $\phi\colon \mathbb R \to \mathbb C$ which takes values on the unit circle in $\mathbb C$ and such that $\phi(x+y)=\phi(x)\phi(y)$.
The constant $\pi$ is defined as being $\tau/2$ when choosing such a unit of measure so that
$$
\lim_{x\to 0} \frac{\sin x}{x} = 1.
$$
This last property of trigonometric functions settles the radian as natural unit for angles in the same way that the corresponding limit
$$
  \lim_{x\to 0} \frac{a^x-1}{x}=1
$$
settles $a=e$ as the natural base of logarithms.
Additional thoughts

*

*I know that by defining the exponential complex function $\exp(z)= \sum_{k=0}^{+\infty} \frac{z^k}{k!}$ we can define everything at once: real exponential, trigonometric function, $e$ and $\pi$. However I find interesting to follow the usual elementary definition of such functions and to settle it rigorously.


*the analogous problem for the exponential function is solved by proving that the limit
$$
  \lim_{n\to +\infty}\left(1+\frac 1 n\right)^n
$$
exists and is finite. Once this is settled to be the number $e$ one can sort of extend this result by monotonicity and find the limit
$$
  \lim_{x\to 0} \left(1+x\right)^{\frac 1 x} = e
$$
which then gives
$$
  \lim_{x\to 0} \frac{\log_e(1+x)}{x} = 1
$$
and finally
$$
  \lim_{x\to 0} \frac{e^x-1}{x} = 1.
$$
Maybe I should find the analogous path for trigonometric functions. In fact using the angle bisection formulas it is easy to show that
$$
  \lim_{n\to \infty}\frac{\sin(2^{-n})}{2^{-n}}
$$
exists because such a sequence is increasing. What I'm missing is to extend such a result to all sequences going to $0$.
 A: I think I have a solution (thanks to Guido de Philippis).
First I want to show that if $x>0$ is sufficiently small for all positive integers $n$ one has:
$$
 \sin x \le n \sin \frac x n \le \tan x.
$$
To prove this let $y=\frac x n$ so that our thesis becomes
$$
\sin ny \le n \sin y \le \tan ny.
$$
We are going to use induction on $n$.
For the first inequality we have
$$
\sin (n+1)y = \sin ny\cdot \cos y + \cos ny \cdot \sin y \le \sin ny + \sin y.
$$
Using inductive assumption we obtain
$$
\sin(n+1)y \le n\sin y + \sin y = (n+1)\sin y
$$
which is what we wanted to prove.
For the second inequality we have:
$$
 \tan (n+1)y = \frac{\tan ny + \tan y}{1 - \tan ny \cdot \tan y} \ge \tan ny + \tan y
\ge \tan ny + \sin y
$$
supposing that $0\le \tan y$, $0\le \tan ny$, $0\le\tan ny \cdot \tan y < 1$.
So by inductive assumption we have
$$
\tan (n+1)y \le n \sin y + \sin y = (n+1)\sin y
$$
as we wanted to prove.
So we have proved that fixed a sufficiently small positive $x$
one has
$$
\frac{\sin x}{x} \le \frac{\sin \frac x n}{\frac x n } \le \frac{\tan x}{x}.
$$
The sequence
$$
  a_n = \frac{\sin \frac x n }{\frac x n}
$$
is increasing (see the answer by Iosif Pinelis). Hence $a_n\to \ell$ with $0 < \ell < +\infty$.
Now given any $y<x$ one can find $n=n(y)$ such that $\frac{x}{n+1} \le y \le \frac{x}{n}$
whence
$$
a_{n+1} \cdot \frac{n}{n+1}
= \frac{\sin \frac x {n+1}}{\frac x n }
\le \frac{\sin y}{y}
\le \frac{\sin \frac x n}{\frac x {n+1}}
= a_n \cdot \frac{n+1}{n}
$$
and now if $y\to 0^+$ one has $n\to +\infty$ hence $\frac{\sin y}{y}\to \ell$.
A: This is to complete the answer by Emanuele Paolini by showing that
\begin{equation*}
    a_n:=\frac{\sin \frac xn}{\frac xn}
\end{equation*}
is increasing in natural $n$ for each $x\in(0,h]$, where $h$ is any positive real number such that $\sin>0$, $\cos>0$, and $\tan<1$ on the interval $(0,h]$.
The desired inequality,
\begin{equation}
a_n<a_{n+1}, \tag{1}\label{1}   
\end{equation}
can be rewritten as
\begin{equation*}
    (n+1)\sin ny>n\sin(n+1)y, \tag{2}\label{2}
\end{equation*}
where $y:=\frac x{n(n+1)}\in(0,\frac h{n(n+1)}]$. Note that
\begin{equation*}
    \sin(n+1)y=\sin ny\cos y+\sin y\cos ny<\sin ny+\sin y\cos ny,
\end{equation*}
so that
\begin{equation*}
    (n+1)\sin ny-n\sin(n+1)y>\sin ny-n\sin y\cos ny \\ 
    =(\tan ny-n\sin y)\cos ny\ge0,
\end{equation*}
in view of the inequality $n\sin y\le\tan ny$ for $y\in(0,\frac hn]$, proved in the answer by Emanuele Paolini.
This proves \eqref{2} and hence \eqref{1}. $\quad\Box$
A: IMHO a theorem that should be in any such course is "Dominated Convergence for Series", since it is easy, it turns out to be useful many times, and it is a toy version of the Lebesgue's convergence theorem. Then, the existence of the limit $\lim_{n\to\infty}(1+z/n)^n$ and its coincidence with the sum of the exponential series is almost immediate. Of course, one should also spend a couple of hours explaining the interpretation of the complex operations as geometric operations on the plane. With this, $t\mapsto e^{it}$ as a uniform circular motion is clear, and one can  define $\cos t$ and $\sin t$ as the real and imaginary part of $e^{it}$, with all elementary properties, including power series expansions and their remainder estimations (in particular, $\sin t=t+o(t)$ as $t\to0$), even before introducing the derivative (the student will find  these facts again later, in the chapter of differential calculus, and appreciate the power of it).
A: Let me make the opening remark that as expressed in the comments, merely the algebraic identities and the specified values at $x=0$ includes wild examples.
However, as written, your monotonicity requirement implies that your desired limit is equivalent to continuity at $x=0$. Indeed, the sought limit naturally beckons a topological requirement to be able to derive it. Let us first introduce a weaker notion than your monotonicity requirement (see at the end for the proof of inclusion).
Definition:
Say that a function $f$ freely separates a point $x_0$ if there exists a neighborhood $\mathcal{U}$ of $x_0$ such that $f(\mathcal{U})\cap\mathcal{U}=\emptyset$.
To be pedantic, let us also use $S(x)$ and $C(x)$ for your would-be sine and cosine functions, respectively. Then we have
Theorem:
If for some $\varepsilon_0\in(-1,1]$ we have that  $C(x)+\varepsilon_0$ freely separates $x=0$, then in addition to your algebraic identities and specified values at $x=0$, the following are equivalent.

*

*$\lim_{x\to0}\frac{S(x)}{x}$ exists.

*$S$ is (uniformly) continuous in a neighborhood of $0$.

*$S$ is continuous at $x=0$.
Remark: Note that you only need continuity of either of $S$ or $C$ and the continuity of the other follows.
Proof of Theorem: To begin with, observe that the following identity holds from your axiomatic algebraic identities:
$$(S(x)-S(y))(1+C(x-y))=S(x-y)(C(x)+C(y))\,.$$
Now, observe that $C(x)+\varepsilon$ freely separates $0$ for any $\varepsilon\in(\varepsilon_0,1]$ once $C(x)+\varepsilon_0$ freely separates $0$. Hence, let $ \mathcal{U}\ni0$ be open such that $\{C(\mathcal{U})+1\}\cap \mathcal{U}=\emptyset$. Then consider any line segment $\mathcal{L}$ centered at $0$ such that $2 \mathcal{L}\subset\mathcal{U}$. In particular, it follows that $M:=\inf_{z\in2\mathcal{L}}|C(z)+1|>0$.
$1\Longleftrightarrow 2$. For the forward direction, from the above identity, for all (distinct) $x,y\in \mathcal{L}$, we obtain
$$\left|S(x)-S(y)\right|=|x-y|\left|\frac{S(x-y)}{x-y}\right|\left|\frac{C(x)+C(y)}{1+C(x-y)}\right|\le2KM^{-1}|x-y|\,, $$
for some positive constant $K$ independent of $x,y$, which exists because of condition 1. Thus, $f$ is Lipschitz continuous on $\mathcal{L}$. For the backward direction, as you observed, the function $\phi(x):=S(x)+iC(x)$ will be exponential and continuous in some neighborhood of $0$, in which case it is an easy exercise verifying that $\phi$ equals $e^{cix}$ in that neighborhood for some real $c$. The limit in (1.) then follows. (Edit: See my comments below and that of LSpice regarding the OP’s query on complex exponential).
$2\Longleftrightarrow 3$: The forward direction is trivial. For the backward direction, starting with our identity above and the line segment $\mathcal{L}$, we obtain,
$$\left|S(x)-S(y)\right|=|S(x-y)|\left|\frac{C(x)+C(y)}{1+C(x-y)}\right|\le2M^{-1}|S(x-y)|\,, $$
and the (uniform) continuity of $S$ on $\mathcal{L}$ follows from continuity at $0$. QED.
Appendix: To see that your monotonicity requirement implies that $C(x)+\varepsilon_0$ freely separates $x=0$ for some $\varepsilon_0$, suppose otherwise  (in fact, any strict monotonicity about the origin suffices). It suffices to let $\varepsilon_0>0$. Then consider any $x>0$ in the open range $\mathcal{R}$ of strict (increasing) monotonicity and let $\delta_n\ne0$ be a null sequence such that $\liminf_{n\to\infty}C(\delta_n)<0$. By the evenness of $C$, we may assume that $\delta_n>0$ and, without loss of generality, assume $\delta_n, x+\delta_n\in\mathcal{R}$ and $C(\delta_n)<0$ for all $n$. By the monotonicity hypothesis, we know that $S(x)>0$ and $S(x+\delta_n)> S(\delta_n)>0$; however, this leads to the contradiction
$$ 0<S(x+\delta_n )-S(\delta_n) = C(\delta_n)S(x)+(C(x)-1) S(\delta_n)<0 $$
since $C(\delta_n)<0$ and $C(x)\le1$.
A: 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'.
