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


1. $\sin^2 x + \cos^2 x = 1$,
2. $\sin(x+y)=\sin x \cos y + \sin y\cos x$, $\cos(x+y)=\cos x \cos y - \sin x \sin y$,
3. $\sin(0)=0$, $\cos(0)=1$
4. there exists $\tau>0$ such that $\sin$ and $\cos$ are $\tau$-periodic
5. $\sin$ is strictly increasing if restricted to $[-\tau/4,\tau/4]$.


If you prefer, last condition can also be replaced with


6. $\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$.



Axiomatic construction of trigonometric functions
This is to complete the [answer](https://mathoverflow.net/a/426247) 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$


